mlsanityData to 7 Oct 2026

Aristotle: IMO-level Automated Theorem Proving

arXiv 2510.01346 ↗First posted 1 Oct 2025cs.AI cs.CLcited by 47

Not on the map. Why?

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.

Key facts. Cited by 47 papers in the map (data through 7 Oct 2026). Builds on 27 of its 62 references that are in the map. First posted on arXiv 1 Oct 2025.

Builds on

27 of 62 references.

References · 27

  1. 2017Hindsight Experience Replaycited by 1,096
  2. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  3. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  4. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  5. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  6. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 270
  7. 2022Autoformalization with Large Language Modelscited by 252
  8. 2017Thinking Fast and Slow with Deep Learning and Tree Searchcited by 245
  9. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  10. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  11. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  12. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
15 more
  1. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 153
  2. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  3. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  4. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  5. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  6. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  7. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  8. 2024The Surprising Effectiveness of Test-Time Training for Few-Shot Learningcited by 88
  9. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 82
  10. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 78
  11. 2025FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Modelscited by 45
  12. 2025APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoningcited by 34
  13. 2024HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Provingcited by 32
  14. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoningcited by 27
  15. 2025ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Datacited by 23

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2025: 4; 2026: 43.

47 papers.

Sort:

By area:

  1. 2026Automated Conjecture Resolution with Formal Verificationcited by 21
  2. 2025Adaptation of Agentic AI: A Survey of Post-Training, Memory, and Skillscited by 19
  3. 2026A Minimal Agent for Automated Theorem Provingcited by 13
  4. 2026AI co-mathematician: Accelerating mathematicians with agentic AIcited by 13
  5. 2026Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verificationcited by 10
  6. 2026Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibriumcited by 7
  7. 2026LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Provingcited by 7
  8. 2026Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Provingcited by 7
  9. 2026Learning to Repair Lean Proofs from Compiler Feedbackcited by 6
  10. 2026Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematicscited by 5
  11. 2026Formalizing Mathematics at Scalecited by 5
  12. 2026Agentic Code Reasoningcited by 4
35 more
  1. 2026The Agentic Researcher: A Practical Guide to AI-Assisted Research in Mathematics and Machine Learningcited by 4
  2. 2026DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agentcited by 4
  3. 2026Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematicscited by 4
  4. 2026MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematicscited by 3
  5. 2025Pessimistic Verification for Open Ended Math Questionscited by 2
  6. 2025MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verificationcited by 2
  7. 2025G"odel's Poetrycited by 1
  8. 2026Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Modelscited by 1
  9. 2026Pipeline for Verifying LLM-Generated Mathematical Solutionscited by 1
  10. 2026Discovering mathematical concepts through a multi-agent systemcited by 1
  11. 2026Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Searchcited by 1
  12. 2026A Theoretical Framework for Self-Play Theorem Proving Algorithmscited by 1
  13. 2026Artificial Intelligence for Mathematical Reasoning: An Integrated Survey of Language Models, Neuro-symbolic Systems, and Verified Discoverycited by 1
  14. 2026MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysiscited by 1
  15. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontiercited by 1
  16. 2026Prove2Me: An Open Collaborative Platform for Scaling Math Formalizationcited by 1
  17. 2026Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Studycited by 0
  18. 2026Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Proverscited by 0
  19. 2026Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCPcited by 0
  20. 2026PROMISE: Proof Automation as Structural Imitation of Human Reasoningcited by 0
  21. 2026Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1cited by 0
  22. 2026Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discoverycited by 0
  23. 2026Teaching LLMs Program Semantics via Symbolic Execution Tracescited by 0
  24. 2026Mapping Uncharted Symmetries: Machine Discovery in Combinatoricscited by 0
  25. 2026Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problemcited by 0
  26. 2026Automating Formal Verification with Agent-Guided Tree Searchcited by 0
  27. 2026Theoria: Rewrite-Acceptability Verification over Informal Reasoning Statescited by 0
  28. 2026AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanicscited by 0
  29. 2026When Does Structured Knowledge Help Neural Theorem Proving?cited by 0
  30. 2026GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Researchcited by 0
  31. 2026LeanPolish: Verified Supervision for Lean Proof Compressioncited by 0
  32. 2026Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalizationcited by 0
  33. 2026FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verificationcited by 0
  34. 2026Cost-Efficient Theorem Proving via Agent Orchestration in Program Verificationcited by 0
  35. 2026LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphscited by 0