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