Automated theorem provers running on a $5k piece of hardware is a cool version of the future