---
title: "Aristotle: IMO-level Automated Theorem Proving (2025)"
description: "The Harmonic Team presents Aristotle, a system for automated theorem proving that combines… 61 references, cited by 27 papers here."
authors: ["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"]
year: 2025
venue: "arXiv:2510.01346"
source: "https://arxiv.org/abs/2510.01346"
doi: "10.48550/arxiv.2510.01346"
arxiv: "2510.01346"
licence: "CC BY 4.0 (arXiv)"
licence_url: "https://creativecommons.org/licenses/by/4.0/"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/achim-2025-aristotle-imo-level-automated-theorem/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/achim-2025-aristotle-imo-level-automated-theorem/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2025](https://md.research.elamur.ai/free/en/papers/2025/page/4/) / Aristotle: IMO-level Automated Theorem Proving

# Aristotle: IMO-level Automated Theorem Proving

**Authors:** Tudor Achim, Alex Best, [Alberto Bietti](https://md.research.elamur.ai/free/en/authors/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](https://md.research.elamur.ai/free/en/authors/aidan-swope/), Matyas Tamas, Vlad Tenev, Jonathan Thomm, Harold Williams and Lawrence Wu · **Year:** 2025 · **Venue:** [arXiv:2510.01346](https://md.research.elamur.ai/free/en/venues/superintelligence-robotics-safety-alignment/) ([SuperIntelligence - Robotics - Safety & Alignment 2025](https://md.research.elamur.ai/free/en/venues/superintelligence-robotics-safety-alignment/2025/)) · **Licence:** [CC BY 4.0 (arXiv)](https://creativecommons.org/licenses/by/4.0/)

**Links:** [Publisher's page](https://arxiv.org/abs/2510.01346) · [PDF](https://arxiv.org/pdf/2510.01346v2) · [DOI 10.48550/arxiv.2510.01346](https://doi.org/10.48550/arxiv.2510.01346) · [arXiv 2510.01346](https://arxiv.org/abs/2510.01346) · [OpenAlex](https://openalex.org/W4414815946)

**Citations:** 2 citations (OpenAlex, 2026-10-14) · [27](https://md.research.elamur.ai/free/en/papers/achim-2025-aristotle-imo-level-automated-theorem/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
The Harmonic Team presents Aristotle, a system for automated theorem proving that combines natural-language mathematical reasoning with machine-checked proofs in Lean 4 and Mathlib. A problem counts as solved only when the final Lean proof is complete, with no gaps or unsound axioms such as sorryAx. The system has three parts. The first runs Monte Carlo Graph Search at massive parallel scale, steered by a single large transformer that serves as both the policy and the value function. It proposes tactics from the proof state, the action history and, when available, an informal proof. The second is an informal reasoning loop that drafts proofs, splits them into lemmas, formalizes them and revises them using Lean feedback. The third is a separate geometry solver modelled on AlphaGeometry. The model is trained with reinforcement learning and then fine-tuned for contest mathematics. On IMO 2025, Aristotle produced verified formal solutions to five of the six problems, which is gold-medal-equivalent. Formal proofs remove the costly step of human checking, which makes this a step toward AI assistants for real mathematical research.

## Key points
- **IMO results:** Aristotle solved 5/6 IMO 2025 problems with formal proofs, which are published on GitHub. The previous formal state of the art was AlphaProof plus AlphaGeometry-2, at silver level on IMO 2024. ByteDance's Seed-Prover reached gold at the same time but uses whole-proof generation with refinement, whereas Aristotle searches step by step.
- **Graph search:** Lean states that match in goals, local context and variable names are merged, which turns the search tree into a hypergraph.
- **Search strategy:** A PUCT variant takes its prior from the empirical frequency of sampled actions rather than sequence logprobs. Proof search is treated as an AND/OR minimax problem: the system expands the most promising action, then the hardest resulting subgoal. Negated goals are added so the search can also disprove statements.
- **Mathlib contributions:** During training, Aristotle proved results missing from Mathlib, including Niven's theorem, the Gauss–Lucas theorem, and the fact that eigenvalues are roots of the characteristic polynomial. It also contributed lemmas to the Polynomial Freiman-Ruzsa and Generalized Quantum Stein's Lemma projects.
- **Tao's textbook:** While checking Terence Tao's Lean-based real analysis textbook, Aristotle found four exercises that were false as written, giving explicit counterexamples. It also found two exercises with a redundant hypothesis.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [University of Southern California](https://md.research.elamur.ai/free/en/universities/university-of-southern-california/) — University, Los Angeles, United States · 183 works · 37,526 citations
- [Cornell University](https://md.research.elamur.ai/free/en/universities/cornell-university/) — University, Ithaca, United States · 139 works · 65,295 citations
- [University of Waterloo](https://md.research.elamur.ai/free/en/universities/university-of-waterloo/) — University, Waterloo, Canada · 85 works · 15,188 citations
- [California Institute of Technology](https://md.research.elamur.ai/free/en/universities/california-institute-of-technology/) — University, Pasadena, United States · 16 works · 1,291 citations
- [Perimeter Institute](https://md.research.elamur.ai/free/en/labs/perimeter-institute/) — Research institute, Waterloo, Canada · 2 works · 285 citations

Also on the byline: [Harmonic (United States)](https://ror.org/03xdrbh54).

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: 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 and Lawrence Wu. 2025. Aristotle: IMO-level Automated Theorem Proving. arXiv:2510.01346.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{achim2025aristotle,
  title = {{Aristotle: IMO-level Automated Theorem Proving}},
  author = {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 and Lawrence Wu},
  year = {2025},
  doi = {10.48550/arxiv.2510.01346},
  eprint = {2510.01346},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2510.01346}
}
```

- [← previous AgentDropout: Dynamic Agent Elimination for Token-Efficient and High-Performance LLM-Based Multi-Agent Collaboration](https://md.research.elamur.ai/free/en/papers/wang-2025-agentdropout-dynamic-agent-elimination-token/)
- [next → BixBench: a Comprehensive Benchmark for LLM-based Agents in Computational Biology](https://md.research.elamur.ai/free/en/papers/mitchener-2025-bixbench-comprehensive-benchmark-llm/)
- [↑ back to papers of 2025](https://md.research.elamur.ai/free/en/papers/2025/page/4/)

## References

61 references, 38 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Ekin Akyürek, Mehul Damani, Adam Zweiger, Linlu Qiu, Han Guo, Jyothish Pari, Yoon Kim, and Jacob Andreas. The Surprising Effectiveness of Test‑Time Training for Few‑Shot Learning, 2024. URL — [The Surprising Effectiveness of Test-Time Training for Few-Shot Learning](https://md.research.elamur.ai/free/en/papers/akyurek-2024-surprising-effectiveness-test-time-training/) [https://arxiv.org/](https://arxiv.org/) abs/2411.07279. [↗](https://arxiv.org/)
2. Marcin Andrychowicz, Filip Wolski, Alex Ray, Jonas Schneider, Rachel Fong, Peter Welinder, Bob McGrew, Josh Tobin, Pieter Abbeel, and Wojciech Zaremba. [Hindsight Experience Replay](https://md.research.elamur.ai/free/en/papers/andrychowicz-2017-hindsight-experience-replay/). In Advances in Neural Information Processing Systems (NeurIPS) 30, pages 5055–5065, 2017. URL [https://papers.nips.cc/](https://papers.nips.cc/) p… [↗](https://papers.nips.cc/)
3. Thomas Anthony, Zheng Tian, and David Barber. [Thinking Fast and Slow with Deep Learning and Tree Search](https://md.research.elamur.ai/free/en/papers/anthony-2017-thinking-fast-slow-deep-learning/). In Advances in Neural Information Processing Systems 30 (NeurIPS 2017), pages 5360–5370, 2017.
4. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://md.research.elamur.ai/free/en/papers/azerbayev-2023-proofnet-autoformalizing-formally-proving-undergraduate/), 2023. URL https://arxiv.org/abs/2302.12433. [↗](https://arxiv.org/abs/2302.12433)
5. Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, Cheng Ren, Jiawei Shen, Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang, Zhihong Wang, Chenrui Wei, Shufa Wei, Yonghui Wu, Yuchen Wu, Yihang Xia, Huajian Xin, Fan Y… — [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://md.research.elamur.ai/free/en/papers/chen-2025-seed-prover-deep-broad-reasoning/)
6. Yuri Chervonyi, Trieu H. Trinh, Miroslav Olšák, Xiaomeng Yang, Hoang Nguyen, Marcelo Menegali, Junehyuk Jung, Vikas Verma, Quoc V. Le, and Thang Luong. Gold‑medalist Performance in Solving Olympiad Geometry with AlphaGeometry2, 2025. [URL https://arxiv.org/abs/2502.03544](https://md.research.elamur.ai/free/en/papers/chervonyi-2025-gold-medalist-performance-solving-olympiad/). [↗](https://arxiv.org/abs/2502.03544)
7. Adrien Couëtoux, Jean-Baptiste Hoock, Nataliya Sokolovska, Olivier Teytaud, and Nicolas Bonnard. Continuous upper confidence trees. In Proceedings of the 5th International Conference on Learning and Intelligent Optimization (LION’05), pages 433–445, Berlin, Heidelberg, 2011. Springer-Verlag. [find](https://scholar.google.com/scholar?q=Adrien+Cou%C3%ABtoux%2C+Jean%2DBaptiste+Hoock%2C+Nataliya+Sokolovska%2C+Olivier+Teytaud%2C+and+Nicolas+Bonnard%2E+Continuous+upper+confidence+trees%2E+In+Proceedings+of+the+5th+International+Conference+on+Learning+and+I)
8. Johannes Czech, Patrick Korus, and Kristian Kersting. Improving alphazero using monte-carlo graph search. In Proceedings of the 31st International Conference on Automated Planning and Scheduling (ICAPS 2021), pages 103–111, 2021. [find](https://scholar.google.com/scholar?q=Johannes+Czech%2C+Patrick+Korus%2C+and+Kristian+Kersting%2E+Improving+alphazero+using+monte%2Dcarlo+graph+search%2E+In+Proceedings+of+the+31st+International+Conference+on+Automated+Planning+and+Scheduling+%28ICAP)
9. Kefan Dong and Tengyu Ma. [STP: Self-Play LLM Theorem Provers with Iterative Conjecturing and Proving](https://md.research.elamur.ai/free/en/papers/dong-2025-stp-self-play-llm-theorem/), 2025. URL https://arxiv.org/abs/2502.00212. [↗](https://arxiv.org/abs/2502.00212)
10. Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://md.research.elamur.ai/free/en/papers/first-2023-baldur-whole-proof-generation-repair/). In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE 2023), pages 1229–1241. As…
11. Fabian Gloeckle, Jannis Limperg, Gabriel Synnaeve, and Amaury Hayat. ABEL: Sample Efficient Online Reinforcement Learning for Neural Theorem Proving. In NeurIPS 2024 Workshop MATH-AI, 2024. URL [https://openreview.net/forum?id=kk3mSjVCUO](https://openreview.net/forum?id=kk3mSjVCUO). [↗](https://openreview.net/forum?id=kk3mSjVCUO)
12. Google DeepMind. AlphaProof: when reinforcement learning meets formal mathematics. YouTube video, March 2025. URL [https://www.youtube.com/watch?v=TFBzP78Jp6A](https://www.youtube.com/watch?v=TFBzP78Jp6A). Presenter: Thomas Hubert. [↗](https://www.youtube.com/watch?v=TFBzP78Jp6A)
13. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. [Proof Artifact Co-Training for Theorem Proving with Language Models](https://md.research.elamur.ai/free/en/papers/han-2021-proof-artifact-co-training-theorem/), 2021. URL https://arxiv.org/abs/2102.06203. [↗](https://arxiv.org/abs/2102.06203)
14. Harmonic. IMO2025: Harmonic’s IMO 2025 Results (Problems & Proofs in Lean). GitHub repository, 2025. URL [https://github.com/harmonic-ai/IMO2025](https://github.com/harmonic-ai/IMO2025). Contains Lean statements and proofs for Problems 1–5 on IMO 2025. [↗](https://github.com/harmonic-ai/IMO2025)
15. Harmonic. Aristotle Achieves Gold Medal Performance at the IMO. Blog post, July 28, 2025. URL [https://harmonic.fun/news\#blog-post-imo](https://harmonic.fun/news\#blog-post-imo). [↗](https://harmonic.fun/news\#blog-post-imo)
16. Harmonic. Running Lean at Scale. Blog post, September 11, 2025. URL [https://harmonic.fun/news\#](https://harmonic.fun/news\#) blog-post-lean. [↗](https://harmonic.fun/news\#)
17. Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. LISA: Language Models of Isabelle Proofs. In Proceedings of the 6th Conference on Artificial Intelligence and Theorem Proving (AITP 2021), volume 83 of EPiC Series in Computing, pages 378–392. EasyChair, 2021. [find](https://scholar.google.com/scholar?q=Albert+Qiaochu+Jiang%2C+Wenda+Li%2C+Jesse+Michael+Han%2C+and+Yuhuai+Wu%2E+LISA%3A+Language+Models+of+Isabelle+Proofs%2E+In+Proceedings+of+the+6th+Conference+on+Artificial+Intelligence+and+Theorem+Proving+%28AITP+20)
18. Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. [THOR: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://md.research.elamur.ai/free/en/papers/jiang-2022-thor-wielding-hammers-integrate-language/). In Advances in Neural Information Processing Systems 35 (NeurIPS 2022), pages 8360–83…
19. Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/). In International Conference on Learning Representations (ICLR), 2023. URL https:…
20. Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. [HyperTree Proof Search for Neural Theorem Proving](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/). In Advances in Neural Information Processing Systems 35 (NeurIPS 2022), pages 34651–34664, 2022.
21. Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. [HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving](https://md.research.elamur.ai/free/en/papers/li-2024-hunyuanprover-scalable-data-synthesis/), 2024. URL https://arxiv.org/abs/2412.20735. [↗](https://arxiv.org/abs/2412.20735)
22. Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. [Lean-STaR: Learning to Interleave Thinking and Proving](https://md.research.elamur.ai/free/en/papers/lin-2024-lean-star-learning-interleave-thinking/), 2024. URL https://arxiv.org/abs/2407.10040. [↗](https://arxiv.org/abs/2407.10040)
23. Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, and Chi Jin. [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://md.research.elamur.ai/free/en/papers/lin-2025-goedel-prover-frontier-model-open/), 2025. URL https://arxiv.org/abs/2502.07640. [↗](https://arxiv.org/abs/2502.07640)
24. Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yu Chen, Yuntian Liu, Yang Jiao, and Tao Luo. [ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data](https://md.research.elamur.ai/free/en/papers/liu-2025-atlas-autoformalizing-theorems-through-lifting/). 2025. URL https://arxiv.org/abs/2502.05567. [↗](https://arxiv.org/abs/2502.05567)
25. Alexander Meiburg. Two lemmas for approxhom. GitHub pull request \#251 in teorth/pfr, 2025. URL [https://github.com/teorth/pfr/pull/251](https://github.com/teorth/pfr/pull/251). [↗](https://github.com/teorth/pfr/pull/251)
26. Alexander Meiburg. Roots of Matrix.charpoly are the eigenvalues. GitHub pull request \#27118 in leanprover-community/mathlib4, 2025. URL [https://github.com/leanprover-community/mathlib4/](https://github.com/leanprover-community/mathlib4/) pull/27118. [↗](https://github.com/leanprover-community/mathlib4/)
27. Alexander Meiburg. limsup/liminf of f + g when either f or g tends to zero. GitHub pull request \#27115 in leanprover-community/mathlib4, 2025. URL [https://github.com/leanprover-community/mathlib4/](https://github.com/leanprover-community/mathlib4/) pull/27115. [↗](https://github.com/leanprover-community/mathlib4/)
28. Alexander Meiburg. Niven’s theorem. GitHub pull request \#26371 in leanprover-community/mathlib4, 2025. URL [https://github.com/leanprover-community/mathlib4/pull/26371](https://github.com/leanprover-community/mathlib4/pull/26371). [↗](https://github.com/leanprover-community/mathlib4/pull/26371)
29. Alexander Meiburg, Leonardo A Lessa, and Rodolfo R. Soldati. Quantum information in Lean, 2025. URL [https://github.com/Timeroot/Lean-QuantumInfo](https://github.com/Timeroot/Lean-QuantumInfo). [↗](https://github.com/Timeroot/Lean-QuantumInfo)
30. Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu. [MagnusHammer: A Transformer-Based Approach to Premise Selection](https://md.research.elamur.ai/free/en/papers/mikula-2023-magnushammer-transformer-based-approach-premise/), 2023. URL https://arxiv.org/abs/2303.04488. [↗](https://arxiv.org/abs/2303.04488)
31. Azim Ospanov, Farzan Farnia, and Roozbeh Yousefzadeh. [APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning](https://md.research.elamur.ai/free/en/papers/ospanov-2025-apollo-automated-llm-lean-collaboration/). 2025. URL https://arxiv.org/abs/2505.05758. [↗](https://arxiv.org/abs/2505.05758)
32. Stanislas Polu and Ilya Sutskever. [Generative Language Modeling for Automated Theorem Proving](https://md.research.elamur.ai/free/en/papers/polu-2020-generative-language-modeling-automated-theorem/), 2020. URL https://arxiv.org/abs/2009.03393. [↗](https://arxiv.org/abs/2009.03393)
33. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. [Formal Mathematics Statement Curriculum Learning](https://md.research.elamur.ai/free/en/papers/polu-2022-formal-mathematics-statement-curriculum-learning/). In The Eleventh International Conference on Learning Representations (ICLR 2023), 2023. URL [https://openreview.net/forum?id=6CE2L64c0de](https://openreview.net/forum?id=6CE2L64c0de). [↗](https://openreview.net/forum?id=6CE2L64c0de)
34. Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcemen… — [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://md.research.elamur.ai/free/en/papers/ren-2025-deepseek-prover-v2-advancing-formal/)
35. Christopher D. Rosin. Multi-armed bandits with episode context. Annals of Mathematics and Artificial Intelligence, 61:203–230, 2011. doi: 10.1007/s10472-011-9258-6. URL [https://link.springer.com/](https://link.springer.com/) article/10.1007/s10472-011-9258-6. — [doi:10.1007/s10472-011-9258-6](https://doi.org/10.1007/s10472-011-9258-6) [↗](https://link.springer.com/)
36. Ziju Shen, Naohao Huang, Fanyi Yang, Yutong Wang, Guoxiong Gao, Tianyi Xu, Jiedong Jiang, Wanyi He, Pu Yang, Mengzhou Sun, Haocheng Ju, Peihao Wu, Bryan Dai, and Bin Dong. REAL‑Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning, 2025. [URL https://arxiv.org/abs/2505.20613](https://md.research.elamur.ai/free/en/papers/shen-2025-real-prover-retrieval-augmented-lean/). [↗](https://arxiv.org/abs/2505.20613)
37. David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, Timothy Lillicrap, Karen Simonyan, and Demis Hassabis. A general reinforcement learning algorithm that masters chess, shogi, and Go through s… — [doi:10.1126/science.aar6404](https://doi.org/10.1126/science.aar6404) [find](https://scholar.google.com/scholar?q=David+Silver%2C+Thomas+Hubert%2C+Julian+Schrittwieser%2C+Ioannis+Antonoglou%2C+Matthew+Lai%2C+Arthur+Guez%2C+Marc+Lanctot%2C+Laurent+Sifre%2C+Dharshan+Kumaran%2C+Thore+Graepel%2C+Timothy+Lillicrap%2C+Karen+Simonyan%2C+and+De)
38. Terence Tao. Analysis I, volume 37 of Texts and Readings in Mathematics. Hindustan Book Agency, New Delhi, India, 3 edition, 2014. [find](https://scholar.google.com/scholar?q=Terence+Tao%2E+Analysis+I%2C+volume+37+of+Texts+and+Readings+in+Mathematics%2E+Hindustan+Book+Agency%2C+New+Delhi%2C+India%2C+3+edition%2C+2014%2E)
39. Terence Tao, 2025. URL [https://github.com/teorth/analysis](https://github.com/teorth/analysis). [↗](https://github.com/teorth/analysis)
40. Terence Tao. Some corrections. GitHub pull request \#113 in teorth/analysis, 2025. URL [https://github.com/teorth/analysis/pull/113](https://github.com/teorth/analysis/pull/113). [↗](https://github.com/teorth/analysis/pull/113)
41. Terence Tao. Machine‐assisted proof. Notices of the American Mathematical Society, 72(1):6–13, 2025. [find](https://scholar.google.com/scholar?q=Terence+Tao%2E+Machine%E2%80%90assisted+proof%2E+Notices+of+the+American+Mathematical+Society%2C+72%281%29%3A6%E2%80%9313%2C+2025%2E)
42. Terence Tao, Yaël Dillies, et al. Repository for formalization of the Polynomial Freiman-Ruzsa conjecture, 2024. URL [https://teorth.github.io/pfr/](https://teorth.github.io/pfr/). [↗](https://teorth.github.io/pfr/)
43. Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. [An In-Context Learning Agent for Formal Theorem-Proving](https://md.research.elamur.ai/free/en/papers/thakur-2023-context-learning-agent-formal-theorem/). In Proceedings of the 2024 Conference on Language Modeling (COLM 2024), 2024. URL [https://openreview.net/forum?id=V7HRrxXUhN](https://openreview.net/forum?id=V7HRrxXUhN). [↗](https://openreview.net/forum?id=V7HRrxXUhN)
44. The Lean Prover Community. A read-eval-print-loop for Lean 4. GitHub repository, 2023. URL [https://github.com/leanprover-community/repl](https://github.com/leanprover-community/repl). [↗](https://github.com/leanprover-community/repl)
45. Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong. [Solving olympiad geometry without human demonstrations](https://md.research.elamur.ai/free/en/papers/trinh-2024-solving-olympiad-geometry-without-human/). Nature, 625(7961):476–482, 2024. doi: 10.1038/s41586-023-06747-5. URL [https://www.nature.com/articles/s41586-023-06747-5](https://www.nature.com/articles/s41586-023-06747-5). [↗](https://www.nature.com/articles/s41586-023-06747-5)
46. George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. PutnamBench: Evaluating Neural Theorem‑Provers on the Putnam Mathematical Competition, 2024. [URL https://arxiv.org/abs/2407.11214](https://md.research.elamur.ai/free/en/papers/tsoukalas-2024-putnambench-evaluating-neural-theorem-provers/). [↗](https://arxiv.org/abs/2407.11214)
47. Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, et al. DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-Level Value Function. In Proceedings of the 61st Annual Meeting of the Association for Computational… [find](https://scholar.google.com/scholar?q=Haiming+Wang%2C+Ye+Yuan%2C+Zhengying+Liu%2C+Jianhao+Shen%2C+Yichun+Yin%2C+Jing+Xiong%2C+Enze+Xie%2C+Han+Shi%2C+Yujun+Li%2C+Lin+Li%2C+et+al%2E+DT%2DSolver%3A+Automated+Theorem+Proving+with+Dynamic%2DTree+Sampling+Guided+by+Proof%2D)
48. Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, Heng Liao, and Xiaodan Liang. [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://md.research.elamur.ai/free/en/papers/wang-2023-lego-prover-neural-theorem-proving/). In Proceedings of the Twelfth International Conference on Learn…
49. Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, Jianqiao Lu, Hugues de Saxcé, Bolton Bailey, Chendong Song, Chenjun Xiao, Dehao Zhang, Ebony Zhang, Frederick Pu, Han Zhu, Jiawei Liu, Jonas Bayer, Julien Michel, Lo… — [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://md.research.elamur.ai/free/en/papers/wang-2025-kimina-prover-preview-large-formal/)
50. David J. Wu. Monte-Carlo Graph Search from First Principles. KataGo GitHub Documentation. URL [https://github.com/lightvector/KataGo/blob/master/docs/GraphSearch.md](https://github.com/lightvector/KataGo/blob/master/docs/GraphSearch.md). [↗](https://github.com/lightvector/KataGo/blob/master/docs/GraphSearch.md)
51. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. [Autoformalization with Large Language Models](https://md.research.elamur.ai/free/en/papers/wu-2022-autoformalization-large-language-models/). In Advances in Neural Information Processing Systems 35 (NeurIPS 2022), pages 32353–32368, 2022.
52. Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems, 2024. URL — [InternLM2.5-StepProver: Advancing Automated Theorem Proving via Critic-Guided Search](https://md.research.elamur.ai/free/en/papers/wu-2024-internlm2-5-stepprover-advancing-automated/) [https://arXiv.org/abs/2410.15700](https://arXiv.org/abs/2410.15700). [↗](https://arXiv.org/abs/2410.15700)
53. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-advancing-theorem-proving/), 2024. URL https://arxiv.org/abs/2405.14333. [↗](https://arxiv.org/abs/2405.14333)
54. Huajian Xin, Z. Ren, Z. Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, F. Wu, Z. Fuli Luo, and Chong Ruan. DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-… — [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-v1-5-harnessing/)
55. Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Ming Ding. BFS‑Prover: Scalable Best‑First Tree Search for LLM‑based Automatic Theorem Proving, July 2025. — [BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving](https://md.research.elamur.ai/free/en/papers/xin-2025-bfs-prover-scalable-best-first/)
56. Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://md.research.elamur.ai/free/en/papers/yang-2023-leandojo-theorem-proving-retrieval-augmented/). In Proceedings of the 2023 Conference on Neural Information Processing Systems Datasets & Benchmarks Tra…
57. Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, Yandong Wen, Ge Zhang, and Weiyang Liu. [FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models](https://md.research.elamur.ai/free/en/papers/yu-2025-formalmath-benchmarking-formal-mathematical-reasoning/), 2025. URL https://arxiv.org/abs/2505.02735. [↗](https://arxiv.org/abs/2505.02735)
58. Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, and Kun Gai. [LeanAbell-Prover: Posttraining Scaling in Formal Reasoning](https://md.research.elamur.ai/free/en/papers/zhang-2025-leanabell-prover-posttraining-scaling-formal/), 2025. URL https://arxiv.org/abs/ 2504.06122. [↗](https://arxiv.org/abs/)
59. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. [miniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://md.research.elamur.ai/free/en/papers/zheng-2021-minif2f-cross-system-benchmark-formal/). International Conference on Learning Representations (ICLR), 2022. URL [https://openreview.net/forum?id=9ZPegFuFTFv](https://openreview.net/forum?id=9ZPegFuFTFv). [↗](https://openreview.net/forum?id=9ZPegFuFTFv)
60. Yichi Zhou, Jianqiu Zhao, Yongxin Zhang, Bohan Wang, Siran Wang, Luoxin Chen, Jiahui Wang, Haowei Chen, Allan Jie, Xinbo Zhang, Haocheng Wang, Luong Trung, Rong Ye, Phan Nhat Hoang, Huishuai Zhang, Peng Sun, and Hang Li. [Solving Formal Math Problems by Decomposition and Iterative Reflection](https://md.research.elamur.ai/free/en/papers/zhou-2025-solving-formal-math-problems-decomposition/), 2025. U…
61. Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Qiaochu Jiang, and Sean Welleck. [Premise Selection for a Lean Hammer](https://md.research.elamur.ai/free/en/papers/zhu-2025-premise-selection-lean-hammer/). 2025. URL https://arxiv.org/abs/2506.07477. A Contributors and Acknowledgements Contributors, ordered alphabetically by last name: Tudor Achim, Alex Best, Alberto Bietti, Kevin Der,… [↗](https://arxiv.org/abs/2506.07477)

*Updated 3 November 2026*