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

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

## Key facts

- Cited by 31 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 30 of its 75 references that are in the map.
- First posted on arXiv 14 Oct 2025.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)
- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

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

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [The AI Scientist-v2: Workshop-Level Automated Scientific Discovery via Agentic Tree Search](https://mlsanity.com/paper/2504.08066/) (2025)
- [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)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [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)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [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)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2](https://mlsanity.com/paper/2502.03544/) (2025)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Evaluating Language Models for Mathematics through Interactions](https://mlsanity.com/paper/2306.01694/) (2023)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [TacticToe: Learning to Prove with Tactics](https://mlsanity.com/paper/1804.00596/) (2018)
- [LeanAgent: Lifelong Learning for Formal Theorem Proving](https://mlsanity.com/paper/2410.06209/) (2024)
- [APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning](https://mlsanity.com/paper/2505.05758/) (2025)
- [Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs](https://mlsanity.com/paper/2506.19923/) (2025)
- [The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq](https://mlsanity.com/paper/2008.00120/) (2020)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [A Formalization of the Generalized Quantum Stein's Lemma in Lean](https://mlsanity.com/paper/2510.08672/) (2025)
- [A New Algorithm for Computing Branch Number of Non-Singular Matrices over Finite Fields](https://mlsanity.com/paper/2405.07007/) (2024)

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

- [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)
- [A Minimal Agent for Automated Theorem Proving](https://mlsanity.com/paper/2602.24273/) (2026)
- [MerLean: An Agentic Framework for Autoformalization in Quantum Computation](https://mlsanity.com/paper/2602.16554/) (2026)
- [VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean](https://mlsanity.com/paper/2602.18307/) (2026)
- [RMA: an Agentic System for Research-Level Mathematical Problems](https://mlsanity.com/paper/2605.22875/) (2026)
- [The Agentic Researcher: A Practical Guide to AI-Assisted Research in Mathematics and Machine Learning](https://mlsanity.com/paper/2603.15914/) (2026)
- [NeuroClaw Technical Report](https://mlsanity.com/paper/2604.24696/) (2026)
- [Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics](https://mlsanity.com/paper/2606.31134/) (2026)
- [Bolzano: Case Studies in LLM-Assisted Mathematical Research](https://mlsanity.com/paper/2604.16989/) (2026)
- [A Machine-Verified Proof of a Quantum-Optimization Conjecture](https://mlsanity.com/paper/2606.29687/) (2026)
- [Agentic AI for Scalable and Robust Optical Systems Control](https://mlsanity.com/paper/2602.20144/) (2026)
- [LLMs with in-context learning for Algorithmic Theoretical Physics](https://mlsanity.com/paper/2605.08212/) (2026)
- [MechMath: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving](https://mlsanity.com/paper/2603.24465/) (2026)
- [Fine-Tuning Small Reasoning Models for Quantum Field Theory](https://mlsanity.com/paper/2604.18936/) (2026)
- [MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving](https://mlsanity.com/paper/2605.26959/) (2026)
- [Automating Formal Verification with Reinforcement Learning and Recursive Inference](https://mlsanity.com/paper/2605.30914/) (2026)
- [MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis](https://mlsanity.com/paper/2606.13782/) (2026)
- [Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory](https://mlsanity.com/paper/2606.20642/) (2026)
- [LAMP: Lean-based Agentic framework with MCP and Proof Repair](https://mlsanity.com/paper/2606.28841/) (2026)
- [Can AI Follow In Einstein's Footsteps?](https://mlsanity.com/paper/2607.27794/) (2026)
- [FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving](https://mlsanity.com/paper/2608.25220/) (2026)
- [AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics](https://mlsanity.com/paper/2609.05157/) (2026)
- [The Topological Dual of a Dataset: A Logic-to-Topology Encoding for AlphaGeometry-Style Data](https://mlsanity.com/paper/2604.18050/) (2026)
- [Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs](https://mlsanity.com/paper/2604.18587/) (2026)
- [Automating Formal Verification with Agent-Guided Tree Search](https://mlsanity.com/paper/2605.27485/) (2026)
- [Stable Menus of Public Goods: AI-Enabled Progress](https://mlsanity.com/paper/2606.16989/) (2026)
- [When AI meets quantum information: A comprehensive review](https://mlsanity.com/paper/2607.00365/) (2026)
- [Credit Cards, Confusion, Computation, and Consequences: What Can We Uncover About Language Model Reasoning?](https://mlsanity.com/paper/2607.26952/) (2026)
- [ProofEvolve: Neuro-Symbolic Evolution for Formal Automated Theorem Proving](https://mlsanity.com/paper/2608.26334/) (2026)

## Abstract (arXiv)

We present Ax-Prover, a multi-agent system for automated theorem proving in Lean that can solve problems across diverse scientific domains and operate either autonomously or collaboratively with human experts. To achieve this, Ax-Prover approaches scientific problem solving through formal proof generation, a process that demands both creative reasoning and strict syntactic rigor. Ax-Prover meets this challenge by equipping Large Language Models (LLMs), which provide knowledge and reasoning, with Lean tools via the Model Context Protocol (MCP), which ensure formal correctness. To evaluate its performance as an autonomous prover, we benchmark our approach against frontier LLMs and specialized prover models on two public math benchmarks and on two Lean benchmarks we introduce in the fields of abstract algebra and quantum theory. On public datasets, Ax-Prover is competitive with state-of-the-art provers, while it largely outperforms them on the new benchmarks. This shows that, unlike specialized systems that struggle to generalize, our tool-based agentic theorem prover approach offers a generalizable methodology for formal verification across diverse scientific domains. Furthermore, we demonstrate Ax-Prover's assistant capabilities in a practical use case, showing how it enabled an expert mathematician to formalize the proof of a complex cryptography theorem.