TLDR: Aristotle, an AI system by The Harmonic Team, achieved gold-medal-equivalent performance on the 2025 International Mathematical Olympiad by formally solving five out of six problems in Lean 4. It integrates a Lean proof search, an informal reasoning system for lemma generation and formalization, and a dedicated geometry solver. Beyond the IMO, Aristotle has contributed to mathematical libraries and identified errors in textbooks, demonstrating broad mathematical reasoning capabilities.
A new artificial intelligence system named Aristotle, developed by The Harmonic Team, has achieved a remarkable feat: gold-medal-equivalent performance on the 2025 International Mathematical Olympiad (IMO) problems. This breakthrough marks a significant step forward in automated theorem proving, combining the precision of formal verification with the flexibility of informal reasoning.
Aristotle successfully provided correct formal solutions to five out of the six challenging problems from the 2025 IMO, a level of performance previously out of reach for AI systems. This achievement is particularly noteworthy because it involves generating proofs in Lean 4, a machine-verifiable language, ensuring the rigor and soundness of the solutions.
How Aristotle Works
The system is built upon three core components that work in synergy:
1. Lean Proof Search System: This component uses a highly parallel Monte Carlo Graph Search (MCGS) algorithm. It takes a Lean proof sketch and attempts to complete any unproven parts. A large transformer model acts as its policy and value function, predicting Lean tactics based on the current proof state, history, and any available informal proofs.
2. Lemma-based Informal Reasoning System: This is where Aristotle’s human-like reasoning comes into play. It generates informal proofs for mathematical statements, breaks them down into smaller, manageable lemmas, and then formalizes these lemmas into Lean. The system iterates on this process, refining its approach based on formal feedback, effectively learning from its own attempts and errors.
3. Dedicated Geometry Solver: For geometry problems, Aristotle employs a specialized solver called Yuclid. This solver is based on a deductive database and algebraic reasoning (DD/AR) engine, offering significant speed advantages over previous systems. Yuclid incorporates various performance optimizations and extensions, allowing it to tackle complex plane geometry problems efficiently.
Also Read:
- HILBERT: Combining AI Intuition and Rigor for Advanced Math Proofs
- EvolProver: A New Approach to Building Robust AI for Formal Mathematics
Beyond the Olympiad
While its IMO performance is a highlight, Aristotle’s capabilities extend far beyond contest mathematics. During its training, the system made novel contributions to Mathlib (Lean’s mathematical library) and other open-source repositories. It even identified subtle mistakes in a popular real analysis textbook by Terence Tao, providing explicit counterexamples for false exercises and noting unnecessary hypotheses in others. This demonstrates Aristotle’s proficiency in advanced topics like category theory and homological algebra, hinting at its potential as a valuable research assistant for mathematicians.
The development of Aristotle, alongside other concurrent advancements like ByteDance’s Seed-Prover, highlights a convergent trend in AI research: combining natural language reasoning for problem decomposition with reinforcement learning guided by formal feedback. This hybrid approach appears to be crucial for achieving high levels of formal mathematical reasoning.
For those interested in the technical details and the formal solutions to the IMO 2025 problems, the full research paper can be accessed here: Aristotle: IMO-level Automated Theorem Proving.
