Elamur Research⌕
☰
home / papers / 2025 / Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics

Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics

Paper · 2025 · Benjamin Breen, Marco Del Tredici, Jacob McCarran et al.

Summary

Specialized Lean provers such as DeepSeek-Prover, Kimina-Prover and Goedel-Prover do well on math competition benchmarks, but they have three drawbacks. They are tied to a fixed Mathlib version, they lose the ability to use tools and hold a dialogue, and they need heavy infrastructure to run. Ax-Prover takes a different route and requires no training. It connects general-purpose frontier LLMs to Lean through the Model Context Protocol (MCP), using tools from lean-lsp-mcp. Three LLM agents divide the work: an Orchestrator, a Prover and a Verifier. They loop until a proof compiles with no errors. The authors evaluated the system on NuminaMath-LEAN and PutnamBench, and they built two new benchmarks, AbstractAlgebra and QuantumTheorems. Ax-Prover was the strongest prover without domain-specific training on the public sets, and it clearly beat all baselines on the new ones. Two cryptography case studies show it as an interactive assistant for researchers who do not know Lean. Overall, the work suggests that tool-equipped general LLMs can carry formal verification beyond pure mathematics.

Key points

  • Architecture: Orchestrator, Prover and Verifier agents work in a closed feedback loop. Through MCP, the Prover can inspect goals, search for lemmas, locate errors and check proofs.
  • Motivation: The authors give an example of Mathlib brittleness. DeepSeek-Prover-V2-671B, released in April 2025, still used a lemma that had been deprecated in March 2025.
  • New datasets:
    • AbstractAlgebra covers groups, rings and fields in a research-style setting.
    • QuantumTheorems covers formal statements from quantum mechanics.
  • Benchmark results: On PutnamBench, Ax-Prover reached the highest accuracy among fully open-sourced agents.
  • Case studies:
    • Ax-Prover formalized an alternate definition of a matrix's branch number in about 2 days on a laptop. In doing so it exposed a gap in the original proof, which took minima over sets that could be empty, although the final result still holds.
    • It certified the Lo–Chau entropy bound used in QKD security proofs, which also produced reusable lemmas on majorization and Schur-convexity.

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

🎓Massachusetts Institute of TechnologyCambridge · United States274 works · 82,013 citations🤝Institució Catalana de Recerca i Estudis AvançatsBarcelona · Spain7 works · 462 citations

Also on the byline: Institute of Photonic Sciences.

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Benjamin Breen, Marco Del Tredici, Jacob McCarran, Javier Aspuru Mijares, Weichen Winston Yin, Kfir Sulimany, Jacob M. Taylor, Frank H. L. Koppens and Dirk Englund. 2025. Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics. arXiv:2510.12787.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2510.12787 · arXiv 2510.12787

@misc{breen2025ax,
  title = {{Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics}},
  author = {Benjamin Breen, Marco {Del Tredici}, Jacob McCarran, Javier Aspuru Mijares, Weichen Winston Yin, Kfir Sulimany, Jacob M. Taylor, Frank H. L. Koppens and Dirk Englund},
  year = {2025},
  doi = {10.48550/arxiv.2510.12787},
  eprint = {2510.12787},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2510.12787}
}

References

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

  1. Mathematics (arxiv archive). arXiv, 2025. Accessed: 2025-09-24. find
  2. Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Mathı̈s Fédérico, Sergei Gukov, Daniel Halpern-Leistner, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, et al. Aristotle: Imo-level automated theorem proving. arXiv preprint arXiv:2510.01346, 2025.
  3. Anthropic. Claude 3.7 sonnet and claude code. claude-3-7-sonnet, 2025. Accessed: 2025-09-16. https://www.anthropic.com/news/ ↗
  4. Anthropic. Claude 4. https://www.anthropic.com/news/claude-4, 2025. Accessed: 2025-09-16. ↗
  5. Anthropic. Claude documentation, 2025. Accessed: 2025-09-19. find
  6. Anthropic. Claude opus 4.1. https://www.anthropic.com/news/claude-opus-4-1, 2025. Accessed: 2025-10-14. ↗
  7. Anthropic PBC. Introducing claude haiku 4.5, October 2025. Accessed on May 25, 2026. find
  8. Kaito Baba, Chaoran Liu, Shuhei Kurita, and Akiyoshi Sannai. Prover agent: An agent-based framework for formal mathematical proofs. arXiv preprint arXiv:2506.19923, 2025.
  9. Haniel Barbosa, Clark Barrett, Pascal Fontaine, and Andrew Reynolds. Satisfiability modulo theories: An appetizer. Communications of the ACM, 65(6):69–77, 2022. find
  10. Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. Computer-aided security proofs for the working cryptographer. In Annual Cryptology Conference, pages 71–90. Springer, 2011. find
  11. Lasse Blaauwbroek, Josef Urban, and Herman Geuvers. The tactician: A seamless, interactive tactic learner and prover for coq. In International Conference on Intelligent Computer Mathematics, pages 271–277. Springer, 2020. find
  12. Bruno Blanchet. A computationally sound mechanized prover for security protocols. IEEE Transactions on Dependable and Secure Computing, 5(4):193–207, 2008. find
  13. Julia Borghoff, Anne Canteaut, Tim Güneysu, Elif Bilge Kavun, Miroslav Knežević, Lars R. Knudsen, Gregor Leander, Ventzislav Nikov, Christof Paar, Christian Rechberger, Peter Rombouts, Søren S. Thomsen, and Tolga Yalçın. Prince – a low-latency block cipher for pervasive computing applications. I… find
  14. Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, et al. Seed-prover: Deep and broad reasoning for automated theorem proving. arXiv preprint arXiv:2507.23726, 2025.
  15. Mark Chen et al. Evaluating large language models trained on code. In arXiv preprint arXiv:2107.03374, 2021.
  16. Yilei Chen. Quantum algorithms for lattice problems. Technical report, Cryptology ePrint Archive, Report 2024/555, 2024. Updated April 18: algorithm contains an unfixable bug invalidating the main claim (see Section 3.5.9, Page 37). find
  17. 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. arXiv preprint arXiv:2502.03544, 2025.
  18. Katherine M Collins, Albert Q Jiang, Simon Frieder, Lionel Wong, Miri Zilka, Umang Bhatt, Thomas Lukasiewicz, Yuhuai Wu, Joshua B Tenenbaum, William Hart, et al. Evaluating language models for mathematics through interactions. Proceedings of the National Academy of Sciences, 121(24):e2318124121, 202…
  19. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 337–340. Springer, 2008. find
  20. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Deduction – CADE-25, volume 9195 of Lecture Notes in Computer Science, pages 378–388. Springer, 2015. find
  21. DeepSeek-AI. Deepseek-prover-v1 dataset. https://huggingface.co/datasets/deepseek-ai/ DeepSeek-Prover-V1, 2024. Accessed: 2025-08-24. ↗
  22. deepseek ai. Deepseek-prover-v2-671b, 2025. Accessed: 2025-09-24. find
  23. Oliver Dressler. Lean-lsp-mcp: Tools for agentic interaction with the lean theorem prover, 3 2025. Accessed: 2025-08-24. find
  24. David S Dummit and Richard M Foote. Abstract algebra. john wile & sons. Inc., Hoboken, NJ, 2004. find
  25. Praveen Gauravaram, Lars Knudsen, Krystian Matusiewicz, Florian Mendel, Christian Rechberger, Martin Schläffer, and Søren S. Thomsen. Grøstl – a sha-3 candidate. Submission to nist, NIST, September 2008. Available at http://www.groestl.info/. ↗
  26. Thérèse Gauthier, Cezary Kaliszyk, and Josef Urban. Tactictoe: Learning to prove with tactics. In Proceedings of the International Conference on Automated Deduction (CADE), pages 275–294. Springer, 2021. find
  27. Juraj Gottweis, Wei-Hung Weng, Alexander Daryin, Tao Tu, Anil Palepu, Petar Sirkovic, Artiom Myaskovsky, Felix Weissenberger, Keran Rong, Ryutaro Tanno, et al. Towards an ai co-scientist. arXiv preprint arXiv:2502.18864, 2025.
  28. Daniel Huang et al. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning (ICML), pages 2654–2663, 2019.
  29. Geoffrey Irving, Christian Szegedy, Alexander A. Alemi, et al. Deepmath - deep sequence models for premise selection. In Advances in Neural Information Processing Systems (NeurIPS), pages 2235–2243, 2016.
  30. Neal Koblitz and Alfred J Menezes. Another look at” provable security”. Journal of Cryptology, 20(1):3–37, 2007. find
  31. Laura Kovács and Andrei Voronkov. First-order theorem proving and vampire. In Proceedings of the International Conference on Computer Aided Verification (CAV), pages 1–35. Springer, 2013. find
  32. Adarsh Kumarappan, Mo Tiwari, Peiyang Song, Robert Joseph George, Chaowei Xiao, and Anima Anandkumar. Leanagent: Lifelong learning for formal theorem proving. arXiv preprint arXiv:2410.06209, 2024. find
  33. Lean Prover Community. Mathlib statistics. https://leanprover-community.github.io/ mathlib_stats.html, 2025. GitHub repository for generating statistics plots for Mathlib; accessed 2025-08-24. ↗
  34. Jia LI, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Costa Huang, Kashif Rasul, Longhui Yu, Albert Jiang, Ziju Shen, Zihan Qin, Bin Dong, Li Zhou, Yann Fleureau, Guillaume Lample, and Stanislas Polu. Numinamath. [https://huggingface.co/AI-MO/NuminaMath-1.5](https://github.c… find
  35. Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640, 2025.
  36. Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, et al. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv preprint arXiv:2508.03613, 2025.
  37. Hoi-Kwong Lo and HF Chau. Unconditional security of quantum key distribution over arbitrarily long distances. arXiv preprint quant-ph/9803006, 1998. find
  38. Hoi-Kwong Lo and Hoi Fung Chau. Unconditional security of quantum key distribution over arbitrarily long distances. science, 283(5410):2050–2056, 1999. find
  39. Zeyuan Lu, Guodong Zhang, Junxiao Chen, Huan Chen, Yilun Chen, Zonglin Li, Yiping Li, Lianmin Wang, Yao Lin, Ce Zhang, and Jie Chen. Process-driven autoformalization in lean 4. In The Thirteenth International Conference on Learning Representations, 2025.
  40. Math Inc. Introducing gauss, an agent for autoformalization, 2025. Announcement of autoformalization agent for formal verification in mathematics. find
  41. Alex Meiburg, Leonardo A Lessa, and Rodolfo R Soldati. A formalization of the generalized quantum stein’s lemma in lean. arXiv preprint arXiv:2510.08672, 2025. — [arXiv:2510.08672](https://arxiv.org/abs/2510.08672) find
  42. P. R. Mishra, Yogesh Kumar, Susanta Samanta, and Atul Gaur. A new algorithm for computing branch number of non-singular matrices over finite fields. arXiv preprint arXiv:2405.07007, 2024. — [arXiv:2405.07007](https://arxiv.org/abs/2405.07007) find
  43. Model Context Protocol. What is the model context protocol (mcp)? https://modelcontextprotocol.io/docs/getting-started/intro, 2024. Accessed: 2025-10-05. ↗
  44. Arvind Narayanan and Vitaly Shmatikov. Robust de-anonymization of large sparse datasets. In 2008 IEEE Symposium on Security and Privacy (sp 2008), pages 111–125. IEEE, 2008. find
  45. National Institute of Standards and Technology. Advanced encryption standard (aes). Federal Information Processing Standards Publication FIPS 197-upd1, U.S. Department of Commerce, Gaithersburg, MD, 2001. Published November 26, 2001; Updated May 9, 2023. find
  46. Michael A Nielsen and Isaac L Chuang. Quantum computation and quantum information. Cambridge university press, 2010. find
  47. Numina-Team. Numinamath-lean dataset. https://huggingface.co/datasets/AI-MO/ NuminaMath-LEAN, 2025. Accessed: 2025-08-24. ↗
  48. OpenAI. Openai models documentation, 2025. Accessed: 2025-09-19. find
  49. Azim Ospanov, Farzan Farnia, and Roozbeh Yousefzadeh. Apollo: Automated llm and lean collaboration for advanced formal reasoning. arXiv preprint arXiv:2505.05758, 2025.
  50. Stanislas Polu et al. Formal mathematics statement curriculum learning. In Advances in Neural Information Processing Systems (NeurIPS), 2023.
  51. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. In International Conference on Learning Representations (ICLR), 2020.
  52. Z.Z. Ren, Zhihong Shao, Wenfeng Liang, et al. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. https://arxiv.org/abs/2504.21801, 2025. Accessed: 2025-08-24. ↗
  53. Sébastien Rousseau. Bug discovered in quantum algorithm for lattice-based crypto. https://sebastienrousseau.com/2024-04-22-bug-discovered-in-quantum-algorithm-for-lattice-based index.html, April 22 2024. Accessed: [add access date here]. ↗
  54. Peter W Shor and John Preskill. Simple proof of security of the bb84 quantum key distribution protocol. Physical review letters, 85(2):441, 2000. find
  55. Victor Shoup. Sequences of games: a tool for taming complexity in security proofs. cryptology eprint archive, 2004. find
  56. Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Lean copilot: Large language models as copilots for theorem proving in lean. arXiv preprint arXiv:2404.12534, 2024.
  57. Latanya Sweeney. k-anonymity: A model for protecting privacy. International journal of uncertainty, fuzziness and knowledge-based systems, 10(05):557–570, 2002. find
  58. Trishullab. Putnambench leaderboard. https://trishullab.github.io/PutnamBench/ leaderboard.html, 2025. Accessed: 2025-10-07. ↗
  59. 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. Advances in Neural Information Processing Systems, 37:11545–11569, 2024.
  60. Sumanth Varambally, Thomas Voice, Yanchao Sun, Zhifeng Chen, Rose Yu, and Ke Ye. Hilbert: Recursively building formal proofs with informal reasoning. arXiv preprint arXiv:2509.22819, 2025.
  61. Haiming Wang et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. https://arxiv.org/abs/2504.11354, 2025. Accessed: 2025-08-24. ↗
  62. Qihao Wu, Haotian Zhang, Jialin Chen, Yizhou Li, Xingjian Zhang, Ce Zhang, and Jie Chen. Autoformalization in the era of large language models: A survey. arXiv preprint arXiv:2505.23486, 2025.
  63. 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://arxiv.org/abs/2405.14333, 2024. Accessed: 2025-08-24. ↗
  64. Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Deepseek-prover-v1. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08152, 2024.
  65. Zhangir Xin et al. Leandojo: Theorem proving with large language models. In International Conference on Learning Representations (ICLR), 2024. find
  66. Yutaro Yamada, Robert Tjarko Lange, Cong Lu, Shengran Hu, Chris Lu, Jakob Foerster, Jeff Clune, and David Ha. The ai scientist-v2: Workshop-level automated scientific discovery via agentic tree search. arXiv preprint arXiv:2504.08066, 2025.
  67. Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. https://arxiv.org/abs/2406. 03847, 2024. Accessed: 2025-08-24. ↗
  68. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: A cross-system benchmark for formal olympiad-level mathematics. https://arxiv.org/abs/2109.00110, 2021. Accessed: 2025-08-24. ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/breen-2025-ax-prover-deep-reasoning-agentic/