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

TL;DR

Ax-Prover presents a novel agentic workflow that unites frontier LLMs with Lean's formal verification via MCP to perform cross-domain theorem proving across mathematics and quantum physics. The system deploys three roles—Orchestrator, Prover, and Verifier—coupled with MCP tools to iteratively generate, check, and refine Lean proofs, while remaining lightweight and accessible via API. Evaluations on public math benchmarks and two new domain datasets (AbstractAlgebra and QuantumTheorems) plus PutnamBench show competitive or superior performance to open-source baselines and specialized provers, with strong generalization to domains beyond Mathlib. Case studies in classical cryptography and quantum cryptography demonstrate practical, interactive verification workflows that surface gaps in informal arguments and produce reusable Lean certificates, highlighting Ax-Prover as a scalable, tool-augmented assistant for rigorous scientific reasoning.

Abstract

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.

Figures (2)

• Figure 1: Left: the multi-agent workflow of Ax-Prover. Right: the tool-enhanced reasoning of the Prover.
• Figure 2: The main steps performed by the Prover to prove a theorem.