Source-linked AI summary
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
TL;DR
Formal mathematical reasoning is a central objective for machine learning because it supports empirical sciences and bottlenecks theoretical sciences. Aristotle combines informal reasoning with Lean 4 formal verification and achieves gold-medal-level performance on the 2025 IMO problems. Its broader training also supports contributions to Mathlib and advanced mathematical reasoning.
Problem
Formal mathematical reasoning is central to empirical science and a bottleneck in many theoretical sciences, motivating automated theorem proving.
Method
Aristotle integrates informal, human-like reasoning with Lean 4 formal verification and uses Monte Carlo Graph Search over equivalent proof states and actions.
Results
Aristotle achieved gold-medal-level performance on the 2025 IMO problems by providing correct formal solutions to five of six problems.
Takeaways & Limitations
Aristotle’s contributions to Mathlib and proficiency in advanced topics indicate broader mathematical reasoning beyond contest problems.
Takeaways & Limitations
AI-generated informal proofs can contain subtle language errors, including confusion among different meanings of “decreasing sequences.”
Abstract
from arXiv · showhide
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.
1 Introduction
Aristotle targets formal mathematical reasoning by combining Lean verification with informal reasoning and a geometry solver. The system achieves gold-medal-equivalent performance on the 2025 IMO and demonstrates favorable scaling for automated theorem proving.
- Motivation and contributions: Aristotle provides correct formal Lean solutions to five of the six 2025 IMO problems, achieving gold-medal-equivalent performance.Human contestants received gold medals for perfect scores on five problems; Aristotle did not solve the final problem.
- Motivation and contributions: Formal mathematical reasoning uses machine-verifiable proofs, such as Lean 4 proofs, rather than only natural-language reasoning.Lean verification supplies a fast reward signal and supports formal verification as a mathematical tool.
- System architecture: Aristotle combines Lean proof search, lemma-based informal reasoning with formal feedback, and a dedicated plane-geometry solver.The informal system generates proofs, decomposes them into lemmas, formalizes them into Lean, and iterates using formal feedback.
- System architecture: The Lean proof search system uses highly parallel Monte Carlo Graph Search with a transformer policy and value function conditioned on Lean proof states and proof history.Available informal proofs can also condition tactic prediction.
- Results: Although evaluated with contest-mathematics fine-tuning, Aristotle was trained broadly on formal mathematics and showed capability beyond contest problems.Reported examples include contributions to Mathlib, textbook error detection, category theory, and homological algebra.
- Results: Aristotle reaches state-of-the-art automated theorem proving performance and demonstrates favorable scaling for Monte Carlo search over possible proof steps.The paper presents both system-level performance and scaling as main contributions.
2 Approach
This section describes the different systems that comprise Aristotle.
- 2 Approach: The section provides a more detailed description of Aristotle’s constituent systems.
- 2 Approach: Aristotle is presented as a system composed of multiple interacting subsystems.
- 2 Approach: The discussion focuses on the systems that make up Aristotle rather than on a single standalone component.
2.1 Search Algorithm
Aristotle’s proof search explores Lean tactic programs with Monte Carlo Graph Search, representing branching goals as a hypergraph and using learned guidance. Test-time training further improves efficiency, specialization, and reuse of proof strategies.
- Search and guidance: Monte Carlo Tree Search uses a generative policy and learned value function to choose Lean tactics from the current proof state and history.The search accepts Lean code containing unproved goals and progressively samples from Lean’s tactic action space.
- States and actions: Actions are Lean-code fragments that can produce multiple resulting states, creating a search hypertree whose branches represent tactic outcomes.The figure illustrates cases splitting one proof state into independently resolved states.
- Equivalences and graph search: Equivalent Lean states and actions are merged, turning the search hypertree into a search hypergraph and enabling Monte Carlo Graph Search.State equivalence uses goal expressions, local-context expressions, and local variable names; action equivalence uses resulting state transitions.
- Search objective: The AND/OR structure treats a state as proven when one action succeeds, while every resulting state of a successful action must be proven.The algorithm prioritizes promising actions and their most challenging resulting states, while also allocating budget to negated goals for pruning and disproof.
- Test-Time Training: Test-time training improved Aristotle’s efficiency and specialization, including solving difficult problems that the base model could not solve at the same search budget.It also supports learning robust chains of basic commands for new or sparsely supported Lean abstractions.
2.2 Lemma-based Reasoning
Aristotle augments formal proof search with an iterative lemma-based reasoning pipeline that generates, formalizes, verifies, and revises short supporting lemmas. Despite noisy informal proofs and lemma formalizations, proven lemmas can improve search performance over search alone.
- Lemma Generation Pipeline: Candidate lemmas are supplied to the search algorithm before the target theorem, allowing higher-level informal reasoning to guide formal proof search.The search can leverage already proven background results or lemmas tailored to the target theorem.
- Lemma Generation Pipeline: The lemma-based system generates informal proofs, decomposes them into lemmas, formalizes each lemma in Lean, and iterates using formal feedback.The pipeline asks for an informal proof, restructures it into short-proof lemmas, formalizes them, and corrects errors reported by the Lean REPL.
- Lemma Generation Pipeline: Multiple subqueries let the model reflect on and edit its initial informal proofs, lemma decompositions, and formalizations.Corrections are driven by feedback from the Lean REPL.
- Lemma Generation Pipeline: The process is noisy because informal proofs typically contain gaps and lemma formalizations often contain errors even after correction.These issues motivate iterative revision rather than assuming the initial lemma list is reliable.
- Outcome: Correctly formalized lemmas meaningfully improve performance over the baseline search algorithm alone.
- Iterative refinement: Proven and unproven lemmas are annotated after failed attempts, then retained or replaced through a revised lemma-generation and formalization cycle.The revision considers both changing an unworkable strategy and refining a sound strategy into more granular lemmas.
2.3 Geometry
Aristotle’s geometry solver, Yuclid, combines deductive-database and algebraic reasoning with speed-oriented implementations and extensions to AlphaGeometry-1. It solves 17 of 30 AG-30 problems in about 0.4 seconds on one CPU core when numerical diagrams are prebuilt.
- Geometry Solver: Yuclid is a fast C++ deductive-database and algebraic-reasoning engine, reported as up to 500x faster than AlphaGeometry-1.The system is published under Apache 2.0 and is designed with speed optimization throughout.
- Optimizations: Yuclid matches numerically valid configurations before its main deductive-database and algebraic-reasoning loop to avoid redundant later effort.Examples include similar triangles, midpoints, and triangle bisectors.
- Optimizations: The solver deduplicates repeated statements and accelerates algebraic reasoning by retaining echelon forms and reduced equation forms.These structures allow subsequent attempts to resume rather than restart work.
- Performance: 17 out of 30 AG-30 problems are solved by Yuclid in about 0.4s on a single 3.1GHz core when numerical diagrams are prebuilt.The remaining problems are saturated under the reported configuration.
- Extensions: A squared-length AR table efficiently represents the Pythagorean Theorem and its more general form.Yuclid can also wrap AR equations as statements, supporting rules such as the parallelogram law.
- Extensions: The optional law-of-sines extension proves one new AG-30 problem but slows Yuclid by approximately 10x, so it is disabled in the recommended configuration.
3 Results
Aristotle’s evaluation highlights formally verified IMO proofs, unusual proof strategies, error correction through formalization, and broader mathematical capabilities beyond contest problems.
- 3.1 IMO 2025: Aristotle required only one human formalization step: translating each informal IMO statement into a formal statement; generated lemmas were autoformalized.
- 3.1.1 Problem 1: Sunny Lines: Aristotle’s “Sunny Lines” proof used algebraic derangements instead of the geometrically obvious but cumbersome convex-body argument, finding a counterexample through n = 5.
- 3.1.2–3.1.4 Other IMO Problems: Aristotle introduced auxiliary definitions not suggested by problem statements, including a novel set S and an invariant f(k) := k^2/(2k −1).
- 3.1.3 Problem 4: Sums of Three Divisors: Formalization repaired confused distinctions among strictly decreasing, weakly decreasing, and eventually decreasing sequences while preserving the informal proof’s key ideas.
- 3.1.4 Problem 5: Inekoalaty Game: Aristotle deployed advanced and relatively obscure techniques, including calculus, nlinarith, and filter_upwards, in proofs of IMO-level statements.
- 3.2 Other Results: Beyond the IMO, Aristotle proved missing Mathlib theorems, contributed to other formalization repositories, handled advanced topics, and found four false textbook exercises.
4 Related Work
Related systems also reached gold-medal performance on IMO 2025, while differing in proof-generation strategy and verification format.
- Seed-Prover: Seed-Prover shares geometry specialization, informal reasoning with formal feedback, lemma decomposition, and reuse of solved lemmas with Aristotle.
- Comparison with Seed-Prover: Aristotle develops proofs step by step through tree search guided by informal reasoning, whereas Seed-Prover generates and iteratively refines whole proofs.
- Comparison with Seed-Prover: Both Aristotle and Seed-Prover reached gold-medal-level IMO performance at the same time despite their different proof-generation approaches.
- Other Frontier Systems: Google DeepMind and OpenAI also achieved gold medal performance on IMO 2025, but their natural-language solutions were evaluated by human judges rather than formal verification.
- Broader Literature: The related-work discussion situates Aristotle within a large literature on deep learning for automated theorem proving.
5 Conclusion
The paper presents Aristotle as a hybrid system combining informal reasoning, guided formal proof search, and Lean verification, with results extending beyond competitive mathematics.
- 5 Conclusion: Aristotle achieved gold-medal-level performance on the 2025 IMO by integrating informal reasoning with formal verification in Lean 4.
- 5 Conclusion: Its architecture combines proof search for formal proofs with a system that generates and formalizes high-level lemmas.
- 5 Conclusion: Aristotle’s contributions to Mathlib and work on advanced mathematical topics support the paper’s broader research-assistant direction.
- 5 Conclusion: The paper identifies large-scale models, guided search, and formal verification as a path toward increasingly sophisticated automated reasoning and discovery.
A Contributors and Acknowledgements
The paper lists its contributors and acknowledges collaborators, the Lean community, and institutional affiliations.
- Contributors: Contributors are listed alphabetically by last name.
- Affiliations: The listed affiliations include Caltech, Cornell University, the University of Waterloo and Perimeter Institute, and the University of Southern California.
- Acknowledgements: The Harmonic team thanks named collaborators and extends gratitude to the Lean community for foundational contributions.
B Lean Interaction
Aristotle interacts with Lean through a REPL that manages proof states, applies tactics, and verifies completed proofs by running self-contained Lean files.
- REPL operation: The Lean REPL manages goal states and applies tactics to individual proof states, including states initialized from Lean files containing sorrys.It can reconstruct and manipulate proof obligations interactively within Lean.
- Proof verification: Completed proofs are rendered as self-contained Lean files and checked for kernel errors, used axioms, and necessary lemmas.Additional checks verify that tactic-generated proof terms are well typed and catch errors early.
- Distributed execution: The REPL runs on stateless CPU-only machines that can process tactic requests independently and scale with demand in GKE.Each request contains enough information to reconstruct the relevant proof state.
C Example Proofs
Aristotle’s selected proofs span homological algebra and Eisenstein series, illustrating formal reasoning beyond competition mathematics through Lean theorem statements and proof steps.
- Homological algebra: The examples include a homological-algebra exercise involving two short exact sequences and a commutative diagram.The formal theorem assumes exactness-related conditions and bijectivity of the outer vertical maps, then proves bijectivity of the middle map.
- Homological algebra: The homological-algebra proof establishes injectivity and surjectivity of the middle morphism through separate construction steps.The proof uses kernel, range, commutativity, and bijectivity hypotheses to derive these two properties.
- Homological algebra: The surjectivity argument repeatedly lifts elements through the commuting diagram and uses kernel membership to construct the required preimage.The formal steps combine surjectivity, commutativity, exactness, and bijectivity assumptions.
- Eisenstein series: The second example formalizes the modular transformation law for the discriminant Δ = g2^3 - 27g3^2 under τ → -1/τ.The target identity is Δ(-1/τ) = (τ/i)^12 Δ(τ), with τ ≠ 0.
- Eisenstein series: The Eisenstein-series proof derives weight-four and weight-six transformations for g2 and g3, then substitutes them into the discriminant definition.The remaining formal work simplifies infinite sums using reindexing equivalences and algebraic normalization.
- Eisenstein series: The final steps use sum reindexing, field simplification, and the identity Complex.I^-1^12 = 1 to close the discriminant transformation proof.The proof concludes after rewriting the transformed g2 and g3 terms and simplifying algebraically.
D Analysis I Examples
Aristotle’s Analysis I examples include detecting textbook errors, proving results under custom definitions, and identifying assumptions that were unnecessary for valid statements.
- Error detection: Aristotle identified four errors in tested textbook material, and the errors were subsequently corrected.The paper includes formal disproofs among the examples obtained during testing.
- Analysis statements: The supplied examples also contain formal statements about Newton’s approximation and an approximation characterization of HasDerivWithinAt.The characterization is expressed using ε, δ, set membership, and a linear approximation bound.
- Assumption analysis: Two proofs found by Aristotle did not require some stated assumptions, so the corresponding extra assumptions were later removed.The paper notes that such assumptions can sometimes be pedagogically deliberate, but these cases were expected to need them.
- Assumption analysis: Aristotle validates a finite-union result without using the hypothesis n ≥ 1.The theorem concerns closed sets indexed by Fin n and concludes that their union is closed.
- Assumption analysis: Aristotle also proves that a point cannot be both a limit point and an isolated point without using the adherent-point hypothesis.The formal proof directly marks the assumption AdherentPt x X as unnecessary.
- Custom definitions: The examples include proofs involving the custom quotient-based Int definition and demonstrate adaptation to non-standard definitions in context.The section presents order trichotomy and equivalence-preservation arguments for the custom integer construction.