# Aristotle: IMO-level Automated Theorem Proving

arXiv: https://arxiv.org/abs/2510.01346 · HTML: https://mlsanity.com/paper/2510.01346/

## Key facts

- Cited by 58 papers in the map (data through 14 Oct 2026).
- Builds on 27 of its 62 references that are in the map.
- First posted on arXiv 1 Oct 2025.

## Builds on (most cited first, 27 of 27)

- [Hindsight Experience Replay](https://mlsanity.com/paper/1707.01495/) (2017)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Thinking Fast and Slow with Deep Learning and Tree Search](https://mlsanity.com/paper/1705.08439/) (2017)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [The Surprising Effectiveness of Test-Time Training for Few-Shot Learning](https://mlsanity.com/paper/2411.07279/) (2024)
- [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://mlsanity.com/paper/2502.03438/) (2025)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models](https://mlsanity.com/paper/2505.02735/) (2025)
- [APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning](https://mlsanity.com/paper/2505.05758/) (2025)
- [HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving](https://mlsanity.com/paper/2412.20735/) (2024)
- [Leanabell-Prover: Posttraining Scaling in Formal Reasoning](https://mlsanity.com/paper/2504.06122/) (2025)
- [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://mlsanity.com/paper/2502.05567/) (2025)

## Built on by (most cited first, 30 of 58)

- [DeepSeek-V4: Towards Highly Efficient Million-Token Context Intelligence](https://mlsanity.com/paper/2606.19348/) (2026)
- [Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs](https://mlsanity.com/paper/2605.00674/) (2026)
- [Automated Conjecture Resolution with Formal Verification](https://mlsanity.com/paper/2604.03789/) (2026)
- [Advancing Mathematics Research with AI-Driven Formal Proof Search](https://mlsanity.com/paper/2605.22763/) (2026)
- [Adaptation of Agentic AI: A Survey of Post-Training, Memory, and Skills](https://mlsanity.com/paper/2512.16301/) (2025)
- [A Minimal Agent for Automated Theorem Proving](https://mlsanity.com/paper/2602.24273/) (2026)
- [AI co-mathematician: Accelerating mathematicians with agentic AI](https://mlsanity.com/paper/2605.06651/) (2026)
- [LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization](https://mlsanity.com/paper/2606.05400/) (2026)
- [Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification](https://mlsanity.com/paper/2603.19329/) (2026)
- [LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving](https://mlsanity.com/paper/2605.13137/) (2026)
- [Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematics](https://mlsanity.com/paper/2605.13171/) (2026)
- [Formalizing Mathematics at Scale](https://mlsanity.com/paper/2605.29955/) (2026)
- [Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium](https://mlsanity.com/paper/2603.15929/) (2026)
- [Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving](https://mlsanity.com/paper/2606.29493/) (2026)
- [Learning to Repair Lean Proofs from Compiler Feedback](https://mlsanity.com/paper/2602.02990/) (2026)
- [DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent](https://mlsanity.com/paper/2604.26311/) (2026)
- [Prove2Me: An Open Collaborative Platform for Scaling Math Formalization](https://mlsanity.com/paper/2608.28433/) (2026)
- [MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics](https://mlsanity.com/paper/2602.02561/) (2026)
- [Agentic Code Reasoning](https://mlsanity.com/paper/2603.01896/) (2026)
- [The Agentic Researcher: A Practical Guide to AI-Assisted Research in Mathematics and Machine Learning](https://mlsanity.com/paper/2603.15914/) (2026)
- [Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics](https://mlsanity.com/paper/2606.31134/) (2026)
- [Pessimistic Verification for Open Ended Math Questions](https://mlsanity.com/paper/2511.21522/) (2025)
- [MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification](https://mlsanity.com/paper/2512.10187/) (2025)
- [G"odel's Poetry](https://mlsanity.com/paper/2512.14252/) (2025)
- [Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models](https://mlsanity.com/paper/2602.10538/) (2026)
- [Pipeline for Verifying LLM-Generated Mathematical Solutions](https://mlsanity.com/paper/2602.20770/) (2026)
- [Discovering mathematical concepts through a multi-agent system](https://mlsanity.com/paper/2603.04528/) (2026)
- [Early Discoveries of Algorithmist I: Promise of Provable Algorithm Synthesis at Scale](https://mlsanity.com/paper/2603.22363/) (2026)
- [Mapping Uncharted Symmetries: Machine Discovery in Combinatorics](https://mlsanity.com/paper/2605.19063/) (2026)
- [Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search](https://mlsanity.com/paper/2605.20244/) (2026)

## Abstract (arXiv)

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.