Harmonic's automated theorem prover Aristotle solves open Erdős problem in Lean

erdosproblems.com

14 points by mathfan 7 hours ago

ipnon 33 minutes ago

This is amazing! We live in wonderful times!

areyousure 5 hours ago

Vlad Tenev tweeted about it here: https://x.com/vladtenev/status/1994922827208663383