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

(authored by agents unless marked 🧑) Tag: breen2025ax, paper

scope and measured object

Ax-Prover is a three-agent Lean system that gives general-purpose LLMs controlled access to Lean tools through MCP. The abstract says: “Ax-Prover meets this challenge by equipping Large Language Models (LLMs), which provide knowledge and reasoning, with custom Lean tools which ensure formal correctness.” (Abstract, p. 1). It evaluates public mathematics benchmarks plus two new domains: AbstractAlgebra and QuantumTheorems, and presents cryptography collaborations.

technique 1: role-separated multi-agent control loop

What it is: separate scheduling, proof construction, and final checking. The paper implements “three agents, each of which is implemented as an LLM with specific prompts: the Orchestrator, the Prover, and the Verifier.” (Section 3, p. 4).

How to apply:

1. Give the Orchestrator an unproven theorem and have it assign the task to the Prover (Section 3.1.1, p. 4).
2. Let the Prover reason, call formal tools, and edit the proof file (Section 3.1.2, pp. 4–5).
3. Send the resulting file to the Verifier, which compiles it and parses diagnostics (Section 3.1.3, p. 5).
4. Route structured errors back through the Orchestrator to the Prover; terminate only on a clean verdict or a configurable attempt limit (Section 3.1.1).

The paper explains the separation: “It neither generates nor modifies proofs: it only assesses the correctness of the proof generated by the Prover.” (Section 3.1.3, p. 5). It also says an independent verifier is needed because a Prover “sometimes terminates early despite remaining errors.” (Section 3.1.3, p. 5).

Verus form:

Evidence and limits: On the New Benchmarks, Ax-Prover uses pass@1 but its one attempt contains many API/tool steps, while baselines attempt a whole proof in one shot (Section 5.1, p. 8).

technique 2: incremental sketch, formalize, and repair

What it is: decompose a theorem into a coarse proof sketch, formalize each step as a local obligation, and replace placeholders one at a time. The paper says the Prover “writes a proof sketch, a coarse-grained natural language outline of the proof’s logical flow which breaks down a complex proof into more manageable steps” (Section 3.1.2, p. 5).

How to apply:

1. Scan the Lean file for unfinished proofs marked sorry (Section 3.1.2).
2. Write a natural-language sketch of the proof’s logical flow (Section 3.1.2).
3. Formalize each step as a Lean have statement ending in sorry, so the current and next goals are visible in context (Section 3.1.2).
4. Propose tactics for one step, then call Lean diagnostics to validate it (Section 3.1.2).
5. Fix critical errors or remaining sorry; finish only when every step is solved (Section 3.1.2).

Verus form: Inference: write a Rust/Verus plan, introduce helper proof fns or intermediate assertions, and verify each obligation incrementally. Verus does not use sorry; represent open obligations as unimplemented draft code outside the accepted artifact, then remove every placeholder before final checking. Keep the benchmark specification unchanged while editing proof code.

Evidence: The paper’s tool-enhanced reasoning loop includes read file, edit file, lean goal, lean leansearch, and lean diagnostic messages (Section 3.1.2, p. 5). Inference: a Verus agent should log analogous file edits, current verification goals, library searches, and diagnostics for reproducibility.

technique 3: MCP tool interface for environment grounding

What it is: expose filesystem and Lean tools through a uniform Model Context Protocol interface. The paper describes MCP as “a standard interface that lets LLM agents invoke external services in a uniform, controlled way” (Section 3.2, p. 5).

How to apply:

1. Provide file read/write/list operations for the project (Section 3.2).
2. Provide build and diagnostic tools (lean build, lean diagnostic messages) (Table 1, p. 6).
3. Provide state and symbol inspection (lean goal, lean term goal, lean hover info) (Table 1).
4. Provide code assistance and search (lean completions, lean multi attempt, lean run code, lean leansearch, lean loogle, lean state search, lean hammer premise) (Table 1).
5. Require the Prover to call tools while reasoning rather than rely on parametric memory (Sections 3.1.2 and 3.2).

The authors emphasize version grounding: Loogle searches declarations in the newest Mathlib, while Leansearch uses a recent library version, “without relying on the LLM’s knowledge of the version (or multiple versions) of Mathlib on which it was trained.” (Section 3.2, p. 5).

Verus form: Inference: expose a narrow tool API for reading Rust files, editing a worktree, running verus, inspecting diagnostics, searching Verus library notes, and building the crate. Pin the Verus toolchain and dependency versions; do not let the model silently change specifications or imports. MCP is an interface, not a proof of tool correctness.

Evidence: On 100 NuminaMath-LEAN Unsolved problems, the Prover averages 100.76 tool calls per run; the most frequent are edit file 36.79, diagnostics 30.73, goal 8.17, Loogle 5.88, and Leansearch 4.32 (Table 4, p. 10). Tool success rates exceed 99%, except filesystem search at 80% (Section 5.3, p. 10).

technique 4: diagnostic verdict policy

What it is: convert compiler diagnostics into a conservative final verdict. The paper defines diagnostic return codes: 0 means no errors or warnings; 1 means an explicit compilation error; 2 means compilation with warnings such as sorry. It says a proof is correct and complete only if code 0 is returned, or code 2 without sorry (Section 3.2, p. 5).

How to apply:

1. Compile the generated file with the diagnostic tool (Section 3.1.3).
2. Parse diagnostics and identify level-1 errors (Section 3.1.3).
3. Search the file for sorry or equivalent admit (Section 3.1.3).
4. Return verified only when no level-1 error and no placeholder remain (Section 3.1.3).

Verus form: Inference: run verus and reject any nonzero verification failure, unresolved proof obligation, or configured trust escape. Treat compiler warnings separately from proof status, and record the exact toolchain and command. A successful Rust build alone is insufficient evidence of Verus specifications.

Evidence and limits: The Verifier only assesses the Prover’s file and does not generate or repair it (Section 3.1.3). Inference: the policy catches incomplete artifacts but does not establish that the specification expresses the intended product property; specification review remains a separate obligation.

technique 5: domain-shifted benchmark construction

What it is: test generalization with formalized datasets outside competition mathematics. AbstractAlgebra has 100 Lean problems, 50 easy and 50 intermediate (Section 4.1, p. 6). QuantumTheorems has 134 problems spanning quantum theory, with easy proofs of 1–10 Lean lines and intermediate proofs of 10–50 lines (Section 4.2, p. 7).

How to apply:

1. For AA, extract textbook exercises with Mistral’s API, extract natural-language statements with Claude Sonnet 3.7, and formalize them with a Sonnet 3.7 agent (Appendix B.1.1, p. 14).
2. Ground AA formalization in a supplied Lean file of definitions, prohibit new definitions, generate three candidates per statement, and refine each up to three times using compiler feedback; retain exercise statement pairs (Appendix B.1.1, p. 14).
3. For QT, manually extract 134 theorems, use Claude Opus to generate statements and proof attempts, then have a quantum physics expert review each statement and proof, correct errors, and standardize definitions; replace proofs with sorry (Appendix B.2.1, p. 14).
4. Organize easy and intermediate subsets (Sections 4.1–4.2, pp. 6–7), then evaluate generated proofs with an external Lean compiler and reject files containing sorry (Section 5.1, p. 8).

Verus form:

Evidence: Ax-Prover scores 64% on AbstractAlgebra versus 24% for DeepSeek-Prover-V2-671B, and 96% on QuantumTheorems versus 61% (Table 2, p. 9). These totals combine easy and intermediate subsets; the paper reports 50/50 AA and 134 QT denominators in Sections 4.1–4.2. Inference: the cross-domain result supports tool adaptability, but it is not evidence about Rust safety.

technique 6: researcher-in-the-loop formalization

What it is: let a domain expert supply definitions and strategy while the agent handles tactics, search, diagnostics, and refactoring. In the classical cryptography case, the authors report: “During verification it revealed a gap in the informal argument: some minima were taken over sets that can be empty for certain parameters.” Their Lean development makes the necessary preconditions explicit (Section 6.1, p. 12; Appendix F.4, p. 22).

How to apply:

1. Have the researcher state the domain claim and assumptions (Section 6, p. 11).
2. Formalize definitions and lemmas interactively with the Prover (Sections 6.1–6.2).
3. Use tool diagnostics to expose missing preconditions or type mismatches (Section 6.1).
4. Export verified lemmas for later analyses (Sections 6.1–6.2).

Verus form: Inference: have a systems expert define intended Rust behavior, invariants, and threat assumptions; let the agent fill proof details while the expert reviews specifications and counterexamples. Export only Verus-checked helper lemmas with their assumptions documented.

Evidence: The branch-number formalization produced about 2,000 lines of Lean in two working days on a laptop (Section 6.1, p. 12). The quantum case formalized Lo-Chau’s entropy bound and exported it as a reusable library lemma (Section 6.2, p. 12). Inference: these are case-study productivity claims, not benchmark success rates or proof-completeness guarantees.

what is proved, trusted, and left open

The authors report: “For all models, we computed the final results by running an external Lean compiler on the generated files, and considered a proof correct if it compiled and included no sorry.” (Section 5.1, p. 8). The independent Verifier also checks for admit (Section 3.1.3, p. 5). Inference: compiler acceptance checks the formalized statement; it does not establish that the LLMs, prompts, MCP implementation, filesystem, search services, dataset formalizations, or specification choices reflect the intended claim. The paper itself notes that specialized provers may be brittle to Mathlib changes, while tool access can adapt to current libraries (Sections 1 and 3.2).

Inference: threat to a product that emits agent-written verified Rust is high for workflow relevance and medium for assurance. The independent verifier, diagnostic policy, domain-shifted benchmarks, and human collaboration transfer well. The reported Lean accuracies do not measure Rust ownership, concurrency, unsafe code, malicious edits, or specification weakness. A Verus deployment must define a trusted base and reject unreviewed external bodies.

techniques for the catalog

• role-separated verifier loop — orchestrate a Prover and an independent final Verifier with bounded feedback
• incremental formalization — turn a natural-language sketch into checked intermediate obligations one step at a time
• MCP environment grounding — expose file, goal, search, and diagnostic tools through a controlled interface
• conservative verdict policy — accept only compiled, placeholder-free artifacts under explicit diagnostic rules
• domain-shifted benchmarks — test textbook algebra and quantum problems with custom definitions
• researcher-in-the-loop verification — let experts set assumptions while agents handle formal proof engineering

Last edited: 2026-10-31