Harmonic's automated theorem prover Aristotle solves open Erdős problem in Lean(erdosproblems.com)
erdosproblems.com
Harmonic's automated theorem prover Aristotle solves open Erdős problem in Lean
https://www.erdosproblems.com/forum/thread/124#post-1892
2 comments
Vlad Tenev tweeted about it here: https://x.com/vladtenev/status/1994922827208663383
This is amazing! We live in wonderful times!