The artificial intelligence (AI) startup Harmonic recently announced that its AI system, Aristotle, successfully generated a formal proof for Erdős Problem #124. This challenge originates from the famous collection of conjectures posed by mathematician Paul Erdős. Aristotle utilizes Lean, a programming environment that functions as a "proof assistant." This allows the AI to construct valid logical arguments and verify them with absolute precision, reportedly achieving this result without direct human intervention.
"Mathematical superintelligence is getting closer by the minute," Harmonic co-founder Vlad Tenev posted to X, "and I’m confident it will change and dramatically accelerate progress in mathematics and all dependent fields."
The future potential for artificial mathematical superintelligence
Erdős Problem #124 is stated here. A more detailed description of Aristotle's proof is posted as a comment. "I believe this is a faithful formalization of (a strengthening of) the conjecture stated on this page," says Harmonic mathematician Boris Alexeev.
"Erdos... omitted a key hypothesis which made the problem a consequence of a known result (Brown's criterion)," notes top mathematician Terence Tao. "However, this fact was not noticed until Boris Alexeev applied the Aristotle tool to this problem, which autonomously located (and formalized in Lean) a solution to this weaker version of the problem within hours."
So the AI solved a weaker variant of the problem rather than the original, more difficult challenge intended by Erdős. This variant was significantly easier to prove than the original theorem. Despite this, the feat is considered a major milestone. It demonstrates that AI agents are now capable of navigating complex formal systems, understanding mathematical definitions, and autonomously constructing verifiable proofs, a capability that hints at the future potential for artificial mathematical superintelligence.
Harmonic recently raised $120 million in funding "to support our rapid progress in developing the world’s most advanced mathematical reasoning model." Earlier this year, Harmonic announced Aristotle’s gold medal-level performance on the 2025 International Mathematical Olympiad.