An artificial intelligence model developed by Harmonic has solved five of the six problems from the 2025 International Mathematical Olympiad, a performance that would have earned it a gold medal in the competition. The results, verified using the Lean proof assistant, mark a significant step in machine reasoning.
How the AI performed
Harmonic’s model, named Aristotle, tackled the notoriously difficult IMO problems, which are designed to test the world’s top high-school mathematicians. Of the six problems, Aristotle produced correct, verifiable solutions for five. The sixth problem remained unsolved. The company said the solutions were checked using Lean, a formal proof system that ensures mathematical correctness.
What the gold medal means
In the IMO, a gold medal is awarded to contestants who achieve a score in the top percentile. Aristotle’s result — five out of six problems solved — would have placed it among the gold medalists. The IMO 2025 problems covered algebra, geometry, number theory, and combinatorics. The model’s ability to reason across these domains suggests progress in AI’s capacity for structured logical deduction.
Verification through Lean
Lean is an interactive theorem prover that allows mathematicians to write and check formal proofs. By using Lean to verify Aristotle’s solutions, Harmonic ensured that the AI’s reasoning was not just plausible but mathematically rigorous. This approach avoids the pitfalls of hallucinated or incomplete reasoning that can plague large language models.
What’s next for Aristotle
Harmonic has not announced a timeline for releasing Aristotle or its underlying technology. The company is expected to publish a technical paper detailing the model’s architecture and training methods. Researchers in AI and mathematics will be watching closely to see whether the approach can scale to more complex problems — and whether it can solve the one problem that stumped it.
