Harmonic's automated theorem prover Aristotle solves open Erdős problem in Lean (erdosproblems.com) 16 points by mathfan 9mo ago ↗ HN
[–] areyousure 9mo ago ↗ Vlad Tenev tweeted about it here: https://x.com/vladtenev/status/1994922827208663383
2 comments
[ 3.1 ms ] story [ 32.2 ms ] thread