Aristotle: IMO-level Automated Theorem Proving
Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Mathïs Fédérico, Sergei Gukov, Daniel Halpern-Leistner, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, Martin Michelsen, Riley Patterson, Eric Rodriguez, Laura Scharff, Vikram Shanker, Vladmir Sicca, Hari Sowrirajan, Aidan Swope, Matyas Tamas, Vlad Tenev, Jonathan Thomm, Harold Williams, Lawrence Wu
cs.AI
Oct 1, 2025 · v1
TL;DR
Aristotle combines a Lean proof search system with informal reasoning and a geometry solver for IMO-level theorem proving.
Abstract
We introduce Aristotle, an AI system that combines formal verification with informal reasoning, achieving gold-medal-equivalent performance on the 2025 International Mathematical Olympiad problems. Aristotle integrates three main components: a Lean proof search system, an informal reasoning system that generates and formalizes lemmas, and a dedicated geometry solver. Our system demonstrates state-of-the-art performance with favorable scaling properties for automated theorem proving.
Problem
Automated theorem proving at the level of International Mathematical Olympiad problems remained an open challenge, requiring integration of formal verification with informal mathematical reasoning and specialized domain solvers.
Approach
The authors introduce Aristotle, an AI system combining formal verification with informal reasoning. It integrates three main components: a Lean proof search system, an informal reasoning system that generates and formalizes lemmas, and a dedicated geometry solver. The system is designed to demonstrate favorable scaling properties for automated theorem proving.
Results
Aristotle achieves gold-medal-equivalent performance on the 2025 International Mathematical Olympiad problems, demonstrating state-of-the-art performance for automated theorem proving.
