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