Aristotle: IMO-level Automated Theorem Proving | Summary

This article explains the key points of Aristotle: IMO-level Automated Theorem Proving.

• 2025-10-01 (arXiv)
• Achim, Tudor, Best, Alex, Bietti, Alberto, Der, Kevin, Fédérico, Mathïs, Gukov, Sergei, Halpern-Leistner, Daniel, Henningsgard, Kirsten, Kudryashov, Yury, Meiburg, Alexander, et al.
• Harmonic, California Institute of Technology, Cornell University, University of Waterloo and Perimeter Institute, University of Southern California
• Paper
• Project Page

Read this article in Korean

Summary

• Automated theorem proving requires generating difficult mathematical proofs whose correctness can be checked automatically. Aristotle produced machine-verified solutions to five of the six 2025 International Mathematical Olympiad (IMO) problems, matching the paper’s gold-medal comparison of perfect solutions to five problems for human contestants.
• The system combines proof search in Lean 4, a machine-verifiable proof language, with an informal reasoning pipeline that generates and formalizes lemmas, intermediate mathematical statements used to prove a target theorem, and a separate geometry solver. Its learned model proposes proof steps and estimates their prospects, while formal feedback directs search and revision.
• The IMO evaluation used manually formalized problem statements, a search model with over 200B parameters, parallel reasoning pipelines, repeated feedback rounds, and test-time training, retraining on experience collected during inference. The report presents verified proof artifacts and selected mathematical applications, but does not quantify total evaluation compute, elapsed time, or separate performance gains from these components.

1 Introduction

The paper motivates formal mathematical reasoning as a setting where automatic verification supplies a reliable training signal and reduces the burden of checking generated arguments. For non-geometry problems, a solution must be a complete Lean 4 proof using Mathlib, Lean’s mathematical library, without gaps or unsound axioms such as sorryAx, the axiom associated with unfinished proofs; geometry is handled separately but still requires machine verification.

• The three subsystems are parallel Lean proof search, iterative informal reasoning and lemma formalization, and a plane-geometry solver based on AlphaGeometry, a system for solving Olympiad geometry problems.
• The evaluated system was fine-tuned for contest mathematics and also trained on broader formal mathematics. The released IMO proof repository is https://github.com/harmonic-ai/IMO2025.

2.1 Search Algorithm

The proof-search component receives a Lean code block and attempts to replace every sorry, a placeholder for an unfinished proof, with verified code. It builds on Monte Carlo Tree Search (MCTS), search guided by sampled actions and estimated values, using one model for both tactic generation and value estimation.

• A tactic is a Lean command that changes or resolves proof goals. The generative policy, the model’s procedure for proposing actions, samples tactics with progressive widening, expanding the sampled action set as search proceeds, conditioned on the proof state, action history, and an informal proof when available.
• The same model and nearly the same prompt serve policy and value tasks, distinguished by a task token. The value function estimates the prospects of a proof state and guides search, which can operate independently or complete sketches supplied by an outer reasoning process.

2.1.1 States and Actions

Search begins from proof states, collections of goals and their available assumptions, obtained by executing an initial Lean snippet. Multiple goals are split into separate states when they contain no metavariables, unresolved variables that can couple goals; otherwise, the goals remain together, while goals introduced by explicit sorry placeholders must be separate and cannot contain metavariables.

• An action is a Lean code fragment containing one or several tactics and possibly informal comments. Because an action can create several successor states, the search forms a hypertree, a tree whose actions can branch into multiple required subgoals.
• The prompt includes the action history, which the authors report helps reduce circular trajectories and maintain coherent proof strategies. A reference natural-language proof is also included when available.

2.1.2 Equivalences and Graph Search

Aristotle merges states with equal goal expressions, local-context expressions, and local variable names, and merges actions when their resulting transitions are equivalent. This reuse converts the hypertree into a hypergraph, a graph allowing an action to connect to several successor states, making the algorithm a form of Monte Carlo Graph Search (MCGS).

• Equivalent initial states do not always yield equivalent results because tactics such as aesop, an automated Lean proof-search tactic, can depend on global state. The report says this issue is handled in practice without detailing the workaround.
• Worst-case per-step complexity changes from O(D) for trees to O(V) for graphs, where D is graph diameter and V is the number of vertices. The authors report no CPU bottleneck for the graphs encountered in practice.

2.1.3 Search Strategy

Search uses a variant of Predictor Upper Confidence bound applied to Trees (PUCT), a rule that balances estimated action quality with exploration weighted by a prior policy. Aristotle estimates that prior from the empirical frequencies of sampled actions, avoiding sequence log probabilities that can penalize actions with several equivalent textual forms.

• A state succeeds if any action proves it, whereas an action succeeds only when every resulting state is proved. This AND/OR structure leads the algorithm to select actions with the highest upper-confidence bounds and then prioritize successor states with the lowest lower-confidence bounds.
• Each single-goal state also receives a transition corresponding to the goal’s logical negation. Search can spend budget on this transition to disprove statements and prune states.

2.1.4 Interleaving Informal Reasoning

Alongside formal Lean code, the model generates informal comments and uses a hidden reasoning trace before choosing an action, with a dynamically selected thinking budget. Comments remain available in later proof contexts, whereas the hidden trace is not subsequently accessible.

• Formal code, comments, and hidden reasoning are trained together. Comment production is initially enforced manually and later persists under reinforcement learning, training from feedback on search outcomes.
• The authors interpret persistent comments as evidence that informal reasoning helps search and use the dynamic budget to select useful reasoning traces for training. The report provides no controlled ablation, an experiment isolating a component’s contribution, measuring these effects.

2.1.5 Postprocessing

After search, Aristotle applies linter suggestions, automated code-quality recommendations, cleans tactic code, and performs additional offline computation to shorten and simplify proofs. A completed proof is an acyclic subgraph with one source state, one successful action per included state, and every successor state required by each chosen action.

• A state can admit several proofs with different costs. Postprocessing can remove unnecessary action sequences or produce a more efficient proof.

2.1.6 Reinforcement Learning

Training starts from a pretrained large language model and follows expert iteration, repeatedly using search-generated solutions to improve the model that guides subsequent search. Mathematical statements come from open-source and in-house data, with automatic statement formalization, judging through the Lean read-eval-print loop (REPL), an interface for executing Lean code and inspecting proof states, and correction.

• The policy learns from search-discovered proofs filtered for nontriviality. The value function learns from proved states and nearby states that were disproved or remained unproved after substantial effort.
• When an informal proof is available, a judge filters formal proofs that do not follow it faithfully. Proofs of intermediate states are also reused as independent training problems, analogous to Hindsight Experience Replay, reuse of achieved intermediate goals as training targets.

2.1.7 Test-Time Training

Test-time training (TTT) alternates attempts on the target problem and generated lemmas with retraining on extracted search traces if the target remains unsolved. The authors report that TTT solved difficult pre-IMO problems that the base model could not solve at the same search budget, but do not report counts or the added training cost.

• During the IMO evaluation, TTT reportedly accelerated lemma processing and transferred useful experience between different proof sketches.
• TTT also helps the model work with unfamiliar Lean abstractions by learning useful combinations of basic commands from its initial attempts.

2.2 Lemma-based Reasoning

The outer reasoning system supplies the search algorithm with candidate lemmas tailored to the target theorem. Since search accepts existing Lean code containing proved background results, completed lemmas become context for later proof steps.

• The intended benefit is to turn a difficult target into a sequence of smaller formal proof tasks. The authors report improvement over search alone but provide no numerical comparison in this report.

2.2.1 Lemma Generation Pipeline

The pipeline first generates an informal proof, restructures it into dependent lemmas with short individual proofs, formalizes their statements, and corrects errors returned by the Lean REPL. Each stage includes several subqueries for reflection and revision.

• Informal proofs can contain gaps, and lemma statements can remain incorrectly formalized after correction. The authors report that enough useful, correctly formalized lemmas survive to improve search.
• Figure 2 shows the pipeline and its feedback loop. The section’s reference to Figure 1 appears to be a numbering error, since Figure 1 illustrates a propositional proof.

2.2.2 Iteration with Formal Feedback

When a target remains unproved, Aristotle marks the attempted lemmas as proved or unproved, preserves proved lemmas, and proposes additional lemmas. It then formalizes and corrects the new statements before another proof attempt.

• Revision considers two explanations for failure: the informal strategy may be unworkable, or a sound strategy may require finer decomposition into lemmas. The revision prompt asks the model to consider both possibilities.

The diagram separates informal planning and statement correction from formal proof search. Its failure loop shows how an unsuccessful target proof leads to revised lemmas and another attempt, while completed lemmas support later obligations.

2.3 Geometry

The separate geometry subsystem uses Yuclid, a C++ deductive database and algebraic reasoning (DD/AR) engine that combines geometric rules with algebraic deductions. The authors report speedups of up to 500x over AlphaGeometry-1 and release Yuclid under Apache 2.0.

• Yuclid supplies a specialized route for plane geometry outside Lean. The speed claim concerns this engine; the report does not establish a corresponding speedup for the entire Aristotle system.

2.3.1 Performance Optimizations

Yuclid reduces repeated work through numerical rule matching, shared statement-progress records, incremental Gaussian elimination, solving linear systems while reusing prior reductions, and storage of partially reduced equations. With prebuilt numerical diagrams, it solves 17 out of 30 problems in AG-30, the geometry problem set used for this evaluation, and saturates the remaining problems, exhausting available deductions, in about 0.4s on a single 3.1GHz core.

• The numerical matcher identifies configurations whose hypotheses and conclusions hold numerically before deduction. A dictionary shares progress among repeated statements, while cached reduced linear systems and equations let algebraic reasoning resume rather than restart.
• Pending equations are stored centrally and referenced through raw pointers. The stated timing excludes numerical-diagram construction.

2.3.2 Other Features

Yuclid adds an algebraic table for squared lengths, allowing the relation AB ⟂ CD ⇔ AC² + BD² = AD² + BC² alongside the existing length and logarithmic-length tables. Equations can be wrapped as statements, enabling additional geometric laws without introducing rule-specific predicates.

• An optional law-of-sines extension, relating triangle side lengths to the sines of opposite angles, solves one additional AG-30 problem through DD/AR but slows Yuclid by approximately 10x, so the recommended configuration disables it.
• The authors also derive new rules from generated problems with up to 4 points that required auxiliary constructions. Most extensions differ from those introduced in AlphaGeometry-2.

3.1 IMO 2025

Aristotle produced formally verified solutions to Problems 1–5 of IMO 2025 and left Problem 6 unsolved. Humans translated each original problem statement into a formal statement; this was the only human formalization step reported, while lemma statements were automatically formalized.

• For problems requiring identification of an unknown, a language model with basic mathematical programming tools first generated candidates, including c = 4 for Problem 3.
• Maximum performance used a search model with over 200B parameters, many parallel lemma pipelines, repeated formal-feedback rounds, and TTT. The report does not specify total compute, wall-clock time, or whether inference was constrained to human contest time limits.

3.1.1 Problem 1: Sunny Lines

For Sunny Lines, Aristotle avoided a geometric argument about how a line intersects the edges of a triangle, which the authors describe as cumbersome to formalize in Lean. It instead developed an algebraic proof using derangements, permutations without fixed points, and found an explicit counterexample by examining points up to n = 5 that ruled out the construction for all greater n.

• The generated proof departed from common human strategies through an algebraic route that avoided the cited geometric formalization difficulty.

3.1.2 Problem 3: Bonza Functions

Bonza Functions asks for a characterization of functions satisfying bᵃ ≡ f(b)ᶠ⁽ᵃ⁾ (mod f(a)), meaning the two expressions have the same remainder modulo f(a). Aristotle introduced the auxiliary set S and used it in several final lemma proofs, although the problem statement did not suggest this definition.

• The formal definition is def S (f : ℕ+ → ℕ+) : Set ℕ+ := {p | Nat.Prime (p : ℕ) ∧ f (p) > 1}. It collects positive prime inputs whose function values exceed 1.
• This example documents the construction and use of an auxiliary definition within the proof; the report does not establish its novelty beyond this problem-solving context.

3.1.3 Problem 4: Sums of Three Divisors

For Sums of Three Divisors, a problem about an infinite sequence governed by a recurrence involving proper divisors, divisors smaller than the number itself, the informal draft confused strictly decreasing sequences, weakly decreasing sequences, and sequences that decrease at some point. It incorrectly described eventual constancy as compatible with an infinite strictly decreasing sequence of positive integers.

• During formalization, Aristotle repaired this error and related gaps while retaining the draft’s useful ideas. The final informal comments followed the verified Lean proof structure.
• The example documents a correction of an erroneous informal argument during formalization.

3.1.4 Problem 5: Inekoalaty Game

For Inekoalaty Game, Aristotle identified and formalized strategies determining wins and draws, and introduced the auxiliary function f(k) := k√2/(2k − 1). The function served as a useful invariant, a quantity preserved by the relevant proof steps, despite not being suggested by the problem statement.

• An initial proof of lemBazzaObjectiveUpperBound used derivatives to bound Φ(k, q) = √((k − 1)q) + √(2k − q). It was later replaced by a more direct proof using nlinarith, a Lean tactic for nonlinear arithmetic.
• Aristotle used filter_upwards, a tactic for manipulating the filters that express limiting behavior in Mathlib, to prove that f(k) approaches 1/√2. The examples show its use of mathematical techniques beyond those required for a high-school solution.

3.2 Other Results

Beyond contest problems, the report describes proofs of results missing from Mathlib, including Niven’s theorem, the Gauss-Lucas theorem, and the relationship between eigenvalues and roots of the characteristic polynomial. It also reports two contributed lemmas for the Polynomial Freiman-Ruzsa formalization project and several for the Generalized Quantum Stein’s Lemma project.

• Selected advanced examples appear in Appendix C. These are illustrative proofs rather than a systematic evaluation of research-level mathematics.
• On several chapters of Terence Tao’s Lean-based Analysis I textbook, Aristotle found four false exercises with explicit counterexamples and two exercises with unnecessary assumptions, while proving all other exercises presented to it. The total number of tested exercises is not given.

4 Related Work

Seed-Prover also achieved gold-medal-level formal performance on IMO 2025 and shares lemma decomposition, formal feedback, reuse of solved lemmas, and a specialized geometry subsystem. Its central proof-generation approach produces and revises whole proofs, whereas Aristotle constructs proofs through guided stepwise search.

• The paper also discusses OpenAI and Google DeepMind systems whose IMO 2025 solutions were natural-language proofs assessed by human judges. Their verification procedures differ from Aristotle’s machine-checked artifacts.
• The report compares architectures without a controlled evaluation under equal data, compute, or inference budgets.

5 Conclusion

The paper concludes that informal reasoning, formal proof search, and generated lemmas can be integrated to achieve gold-medal-equivalent IMO performance. Mathlib contributions and selected advanced proofs provide additional evidence of use beyond competition mathematics, while broader mathematical research assistance remains a proposed direction.

Appendix

• A Contributors and Acknowledgements lists the Harmonic team’s contributors, identifies several academic affiliations, and acknowledges external contributors and the Lean community.
• B Lean Interaction describes a Lean-written REPL that initializes goals from unfinished files and executes tactics on individual states. Completed proofs are rendered as self-contained Lean files and checked for errors in Lean’s kernel, its trusted proof checker, used axioms, and required lemmas, with additional type checks during search. Stateless requests carry the information needed to reconstruct a proof state and run across CPU-only machines hosted in GKE, the hosting platform the paper says supports demand-based scaling and per-request routing.
• C Example Proofs presents formal_2068504, an exercise in homological algebra concerning maps between algebraic structures. It proves that the middle vertical map is bijective in a commutative diagram, where alternative compositions agree, of short exact sequences, where each map’s image equals the next map’s kernel, when the outer vertical maps are bijective. The second example, formal_2210385, uses Eisenstein series, the lattice-defined sums supplied in the example, to establish the discriminant transformation Δ(−1/τ) = (τ/i)¹²Δ(τ), where Δ = g₂³ − 27g₃² and i is the imaginary unit, under the supplied definitions and τ ≠ 0.
• D Analysis I Examples provides explicit disproofs for four erroneous statements: a strict inequality in a derivative characterization, a derivative claim at a singular point, an isolated-point claim, and a bounded-set statement failing for the empty set. It also shows that n ≥ 1 is unnecessary in Exercise 9.1.7 and AdherentPt x X, the assumption that x lies in the closure of X, is unnecessary in Exercise 9.1.9. Further code proves Int.trichotomous’, which gives the three possible order relations between two integers, and constructs Int.equivInt_ordered_ring, an equivalence preserving order, addition, and multiplication, for the textbook’s custom integer representation.

Brief Thoughts

The checkable proof artifacts establish the reported solutions, and Problem 4 documents the repair of a flawed informal argument during formalization. This example shows how formal proof construction can improve an argument as well as supply a final correctness check.

The report leaves efficiency and component attribution unresolved. Manual input formalization, an over-200B-parameter search model, unspecified parallelism, and unquantified TTT costs limit comparisons with human contest conditions or other systems; controlled ablations and explicit resource budgets would make the scaling claims easier to assess.