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

**Authors:** Marco Del Tredici, Jacob McCarran, Benjamin Breen, Javier Aspuru Mijares, Weichen Winston Yin, Jacob M. Taylor, Frank Koppens, Dirk Englund  
**arXiv:** [2510.12787](https://arxiv.org/abs/2510.12787)  
**Date:** 2025-10-14  
**Summary page:** https://www.summarizepaper.com/en/paper/2510.12787v1/

## Key points

- Development of Large Language Models (LLMs) for reasoning across diverse scientific domains is a significant challenge in automated theorem proving
- Specialized prover models derived from cutting-edge LLMs show impressive performance on math benchmarks but face limitations in adapting to evolving mathematical libraries
- General-purpose LLMs like Claude and GPT possess broad knowledge spanning various domains, exhibit strong natural language understanding and problem-solving skills, but lack explicit training for formalizing statements or constructing proofs in Lean
- Ax-Prover emerges as a multi-agent system designed for automated theorem proving in Lean, bridging the gap between specialized provers and general-purpose LLMs through the Model Context Protocol (MCP)
- Ax-Prover demonstrates competitive performance on public math datasets and showcases superior capabilities on novel challenges, offering a generalizable methodology for formal verification across diverse scientific domains

## Summary

, , , , 

In the field of artificial intelligence, the development of Large Language Models (LLMs) capable of reasoning across diverse scientific domains is a significant challenge in automated theorem proving. While LLM-based formal reasoning systems have made remarkable progress in mathematics, such as with Lean - an open-source programming language and interactive proof assistant - there is still much work to be done to ensure their generalizability beyond specific domains. Specialized prover models derived from cutting-edge LLMs have shown impressive performance on math benchmarks like miniF2F and PutnamBench, but they face limitations in adapting to evolving mathematical libraries like Mathlib. On the other hand, general-purpose LLMs like Claude and GPT possess broad knowledge spanning various domains including mathematics, physics, and computer science. These models exhibit strong natural language understanding and problem-solving skills, making them easily deployable and integratable into different workflows through APIs. However, they lack explicit training for formalizing statements or constructing proofs in Lean, hindering their ability to interface with the formal reasoning infrastructure required for theorem proving. To bridge this gap between specialized provers and general-purpose LLMs, Ax-Prover emerges as a multi-agent system designed for automated theorem proving in Lean. By equipping LLMs with Lean tools via the Model Context Protocol (MCP), Ax-Prover enables formal proof generation that demands both creative reasoning and strict syntactic rigor. Through benchmarking against state-of-the-art provers on public math datasets as well as new benchmarks in abstract algebra and quantum theory fields introduced by researchers themselves, Ax-Prover demonstrates competitive performance while showcasing superior capabilities on novel challenges. Moreover, Ax-Prover's assistant capabilities are highlighted through a practical use case where it aids an expert mathematician in formalizing a complex cryptography theorem. This showcases how Ax-Prover's tool-based agentic approach offers a generalizable methodology for formal verification across diverse scientific domains while enabling collaboration between human experts and AI systems. Overall, Ax-Prover represents a promising advancement towards scalable and flexible automated theorem proving systems that can operate autonomously or collaboratively with human experts across various scientific disciplines.