Harmonic's automated theorem prover Aristotle solves open Erdős problem in Lean (www.erdosproblems.com)

Harmonic’s automated theorem prover Aristotle has independently found a formal proof, checked in Lean, of an Erdős-style conjecture from the Formal Conjectures project. The proven statement (eroded here as erdos_124) says roughly: for any finite family of bases d_i ≥ 2, if ∑ 1/(d_i − 1) ≥ 1, then every natural number n can be written as a sum of k numbers a_i whose base-d_i digit sets are contained in {0,1}. The author corrected a typo in the original formalization (a displayed “≥1” vs Lean’s “=1”), simplified the statement, and Aristotle produced proofs of three variants; the chosen version is a strengthening matching the intended Erdős formulation. This result is significant because it demonstrates an automated prover performing nontrivial, research-level mathematics starting only from a formal statement. Aristotle’s search produced a proof in about six hours, and Lean verified it in roughly one minute — illustrating the practical workflow of AI-guided proof search plus fast machine checking. The note also flags subtle differences between earlier literature formulations (BEGL96 vs Er97) involving unit-digit/power and gcd conditions, underscoring how automated provers can expose and resolve formalization ambiguities. Overall, the episode showcases progress toward trustworthy, autonomous theorem discovery and the growing role of AI tools in formal mathematics.