# AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics

> AxQM introduces the largest physics proof-synthesis benchmark, with 1,019 Lean-verified tasks from Nielsen and Chuang, exposing kernel-evading formalization errors.

- **Source:** [arXiv](https://arxiv.org/abs/2609.05157)
- **Published:** 2026-09-12
- **Permalink:** https://picx.dev/p/J3cn4H
- **Whiteboard:** https://picx.dev/p/J3cn4H/image

## Summary

# AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics

## Summary (Overview)

- **AxQM** is a new benchmark containing **1,019 kernel-checkable proof-synthesis tasks** over **479 items** drawn from Nielsen and Chuang's *Quantum Computation and Quantum Information*—the largest proof-synthesis benchmark in physics by a factor of 4.1× compared to the previous largest (PhysLeanData).
- The benchmark is built on a **custom Lean 4 library** of finite-dimensional quantum mechanics, forked from Mathlib at commit `e560e3ad` (Lean toolchain v4.30.0-rc1), with all reference proofs kept private to prevent data leakage into LLM training corpora.
- Grading is performed **deterministically by the Lean kernel**, checking that proofs compile, contain no `sorry`, and introduce no new axioms—ensuring machine-verified rigor.
- The library exhibits **high interdependency** (median item shares 84% of its dependency closure with other items), providing structural evidence of semantic correctness, though the authors acknowledge that kernel verification cannot catch vacuous or physically unfaithful formalizations.
- The paper also documents **specific failure modes** in physics formalization, including examples of flawed tasks in existing benchmarks (Lean-QIT-Bench, Lean-QuantumAlg-Bench), where quantifier errors or bypassed algorithms evade the Lean kernel.

---

## Introduction and Theoretical Foundation

### Background and Motivation

Formalization in proof assistants like Lean 4 has become a gold standard for machine-checked mathematical rigor. The Lean kernel accepts a proof only after checking every step down to the axioms, shifting the burden of review from "pages of argument" to a single question: *does this formal statement say what it claims?* Recent advances in autoformalization have scaled this from individual theorems to entire textbooks.

Physics stands to benefit even more than mathematics because physical reasoning is rarely expressed at full mathematical rigor. The authors cite two concrete successes:

> Formalizing the stability conditions of the two-Higgs-doublet potential recently exposed an error in a widely cited paper, and a machine-verified proof has settled an open conjecture in quantum optimization.

### Theoretical Foundation

The paper adopts Douglas's framework for formalizing mathematical physics: rigorous statements and proofs are extracted as explicit mathematical premises, with physics entering through **typed hypotheses** and a **dictionary** mapping physical quantities to mathematical objects. The example given is BCS superconductivity:

- **Physical assumptions** (not formalized): effective electron attraction, mean-field restriction
- **Rigorous mathematics** (formalized): from the BCS functional onward—gap equation, energy gap, transition temperature

AxQM applies this split to Nielsen and Chuang's textbook:
- The **postulates of quantum mechanics** enter as primitives
- Each formal statement is a **dictionary entry** tying a textbook claim to a mathematical object
- The Lean kernel checks every proof from that foundation onward

The benchmark is deliberately limited to **finite-dimensional Hilbert spaces**, staying inside Mathlib's finite-dimensional linear algebra library with its spectral theorem, trace, and tensor products—avoiding the functional-analytic hypotheses needed for infinite-dimensional systems.

---

## Methodology

### Benchmark Construction

**Source material**: 687 items extracted from Nielsen and Chuang; 505 formalized; 479 included in the benchmark with tasks.

**Exclusion criteria** (26 of 505 formalized items excluded):
1. Already a theorem in upstream Mathlib
2. Proof needed for another task to compile
3. Definition with no proof to synthesize
4. Duplicate of another item
5. Removed manually for quality

### Library Architecture

The benchmark library adds **3,519 Lean declarations** on top of the Mathlib fork; the full solution library adds **10,560**.

**Proof length estimates** (Table 1):

| Proof length estimate | Tasks | Share |
|---|---|---|
| very small | 158 | 15.5% |
| small | 324 | 31.8% |
| moderate | 280 | 27.5% |
| large | 190 | 18.6% |
| very large | 67 | 6.6% |
| **Total** | **1,019** | **100%** |

The band is assigned from the number of declarations a task's reference proof needs beyond the released benchmark library. The largest reference proof introduced more than 450 declarations.

### Mathlib Fork Justification

All 24 file changes constitute a single refactor: generalizing `MultilinearMap` from a linear map over a single ring in each argument to a **multi-semi-linear map**, where scaling an argument by $c$ scales the value by $\sigma(c)$ for a ring homomorphism $\sigma$. The original Mathlib statement is recovered by setting $\sigma = \text{id}$.

**Why this is necessary**: The inner product on an $n$-ary tensor product of state spaces requires **conjugate-linearity** in each argument of the left factor ($\sigma$ being complex conjugation). This enables using Mathlib's trusted `InnerProductSpace` machinery for multi-party quantum registers without a new separate API for multi-conjugate-linear maps.

This follows the precedent of `LinearMap` being generalized to a semilinear map along an arbitrary ring homomorphism. The refactor is an open pull request on Mathlib (#42534).

### Grading Regime

Grading follows the standard Lean benchmark convention:
1. The library compiles
2. The submitted proof contains no `sorry` in itself or its dependencies
3. No new axioms are added

### Two Benchmark Regimes

- **Independent regime**: each task is completed on its own
- **Dependency-order regime**: prerequisite tasks must be completed first (387 of 1,019 tasks were proved by invoking at least one other task)

---

## Empirical Validation / Results

### Size Comparison with Existing Benchmarks

| Benchmark | Domain | Size |
|---|---|---|
| AxQM | Physics (quantum computing) | **1,019 tasks** |
| PhysLeanData (held-out split) | Physics | 250 |
| Purpose-built physics benchmarks | Physics | ≤ 200 |
| ProofNet | Undergraduate math textbooks | 371 |
| TaoBench | Analysis textbook | 150 |
| Competition math benchmarks | Mathematics | 488–5,560 |

At 1,019 tasks, AxQM is **4.1× the size** of the largest comparable physics evaluation set.

### Library Interdependency Analysis

The paper measures **shared dependency usage** across items (Fig. 2):
- **Median item shares 84% of its dependency closure** with at least one other item
- The most-depended-upon declarations (e.g., Pauli matrices) are used by **over 100 items, up to 159**

This structural argument constrains semantic errors: a definitional error in a foundational declaration would have had to survive every proof that depends on it.

### Chapter-wise Dependency Structure

The dependency matrix between chapters is **close to lower-triangular** (Fig. 3), reflecting the pedagogical structure of the book. For example, there are 15 instances of tasks in chapter 7 directly depending on tasks in chapter 4.

### Coverage

Chapters 1 (overview) and 3 (classical computation) contribute no items. Chapters 7 (physical realization) and 10 (error correction) are densest in tasks per item.

---

## Theoretical and Practical Implications

### Failure Modes in Physics Formalization

The paper identifies critical failure modes that evade the Lean kernel:

**1. Vacuous definitions**: The formal statement does not mean what it purports to mean. Example:

```python
def distanceTraveled (a t: R): R := a * t ^ 2 / 2
theorem distanceTraveled_eq (a t: R):
    distanceTraveled a t = a * t ^ 2 / 2 := rfl
```

This compiles with no `sorry` but is empty of physical content—it defines "distance traveled" to be the result rather than deriving it from the equation of motion $x''(t) = a$, $x(0) = 0$, $x'(0) = 0$.

> Physics is more exposed to this than mathematics for a structural reason... Physics texts speak of both the physical objects and the mathematical objects that model them, often in an interchangeable way. This modeling step is not something a proof assistant can check, even in principle.

**2. Quantifier errors**: Moving a critical logical step into hypotheses or misordering quantifiers. Example from Lean-QIT-Bench's `HamiltonianSimulation/FirstOrderLieTrotterGlobalErrorScaling`:

- Informal: $f(m) \sim O(1/m)$
- Formal: $\forall m \ldots \exists K \ldots f(m) \leq K/m$
- **Error**: $K$ may depend on $m$, making the statement trivially true by $K = m f(m)$

**3. Bypassed algorithms**: In `Fourier/QPESuperpositionExactEigenvectors`, the phase estimation circuit is never constructed in the formal statement—its action is taken as a hypothesis, so the task reduces to a trivial linearity argument.

### Implications

- **For the formal verification community**: AxQM establishes a baseline for textbook-scale physics formalization, with all the expected infrastructure—dependency ledgers, difficulty estimates, and a clear grading protocol.
- **For the AI/ML community**: The benchmark's design (custom library beyond LLM training corpora, private solutions) makes it suitable for evaluating genuine proof-synthesis capability rather than memorization.
- **For the physics community**: The explicit dictionary approach and the documentation of failure modes provide a template for trustworthy formalization in physics, where the kernel alone cannot guarantee semantic correctness.

---

## Conclusion

AxQM is the first **textbook-scale formalization of physics** in a proof assistant: 1,019 tasks over 479 items from Nielsen and Chuang, constructed on a custom Lean library of finite-dimensional quantum mechanics built on a forked Mathlib.

**Key takeaways**:

1. The benchmark is **largest in physics by 4.1×**, spanning density operators, Schmidt decomposition, universal gates, quantum Fourier transform, quantum channels, stabilizer codes, fault tolerance, and von Neumann entropy.
2. The Mathlib fork generalizing `MultilinearMap` to multi-semi-linear maps is a principled, minimal change needed to express inner products on $n$-ary tensor products of quantum state spaces, with potential upstream acceptance into Mathlib.
3. The paper honestly documents the **limits of kernel-based verification**, calling for community review of physical faithfulness—the benchmark's "failure mode that matters."
4. The interdependency analysis (Fig. 2) provides a **structural argument for semantic correctness**: high shared usage constrains the kinds of errors that can persist in the library.

**Future directions**:
- Periodic benchmark updates with community corrections
- Potential rebase to unpinned Mathlib if PR #42534 is accepted
- The authors invite expert review and report submissions via GitHub

The benchmark is publicly available at `https://github.com/Axiomatic-AI/AxQM` under the Apache 2.0 license, with the solution library withheld to prevent LLM training contamination.

---

_Markdown view of https://picx.dev/p/J3cn4H, served by PicX — AI-generated visual whiteboard summaries of research papers._