Aristotle, the AI mathematics system developed by Harmonic, has independently solved a long-standing number theory challenge: Erdős Problem #124, which has remained open since the early 1990s. The AI generated the proof in six hours and then formally verified it using Lean in under a minute. Founder Vlad Tenev called this the emergence of the “vibe proving” era. Source: Erdős Problems Forum.

• Breakthrough: Aristotle solved the full version of Erdős Problem #124, a problem involving complete sequences of sets of integer powers, first posed in the journal Acta Arithmetica.
• Pipeline: The solution came from Aristotle’s upgraded beta model — equipped with stronger reasoning and a natural language interface for step-by-step proof exploration.
• Verification: After generating the proof, Aristotle automatically converted it into Lean code, where it was machine-verified.
• Harmonic’s vision: Tenev described this moment as the start of AI-driven proof discovery, followed by formal verification — a workflow that can operate at superhuman speeds.
• Momentum: This follows Harmonic’s $120M funding and Aristotle’s gold-medal performance on the 2024 IMO reasoning challenge, placing it alongside labs like Google DeepMind and OpenAI in mathematical AI.

Why it matters: Solving an open Erdős problem without human assistance marks a historic shift from “AI that helps mathematicians” to “AI that does original mathematics.” Harmonic’s Aristotle is pushing toward mathematical superintelligence, where proofs can be discovered, verified, and scaled rapidly. This breakthrough could democratize high-level math by turning elite proof work into something accessible to many, not just experts.