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

AI summary

Overview

Research area: Quantum information theory, formal verification (Lean 4 proof assistant), and AI benchmark design for automated theorem proving.

Technical level: Advanced. The paper is written for readers familiar with quantum information concepts and, ideally, with proof assistants; the prose is clear, but the subject matter (kernel-checked proofs, dependent type theory, multilinear maps) is specialist.

One-sentence scope: AxQM is a 1,019-task Lean 4 benchmark, built from 479 numbered items in Nielsen and Chuang's Quantum Computation and Quantum Information, for evaluating systems that automatically synthesize machine-checked proofs in finite-dimensional quantum mechanics.

What This Paper Is About

Large language models can now formalize mathematics at textbook scale, but physics has lacked a rigorous, kernel-checked benchmark for measuring that capability. The authors argue that physics needs this more than mathematics, because physical arguments routinely rely on unstated idealizations and approximations that can hide logical gaps. Their goal is to release a large, guaranteed-solvable, deterministically graded benchmark of formal proof-synthesis tasks drawn from a single foundational quantum computing textbook, together with the custom Lean library those tasks live in.

Key Contributions

1. A textbook-scale benchmark for physics. AxQM contains 1,019 kernel-checkable proof-synthesis tasks over 479 items from Nielsen and Chuang. By task count the authors describe it as the largest proof-synthesis benchmark in physics by a factor of four, and 4.1 times the size of the 250-instance held-out split of PhysLeanData.

2. A purpose-built Lean library of finite-dimensional quantum mechanics. The tasks are stated inside a shared foundational library built on a forked Mathlib, covering density operators, the Schmidt decomposition, universal gate sets, the quantum Fourier transform, order-finding, Grover search, quantum channels and their distance measures, stabilizer codes, fault tolerance, and von Neumann entropy. The benchmark library adds 3,519 Lean declarations on top of the Mathlib fork; the complete library with solutions adds 10,560.

3. A justified Mathlib fork. All 24 file changes are one refactor generalizing MultilinearMap from linearity over a single ring to a multi-semi-linear map, needed to define an inner product on n-ary tensor products of state spaces that is conjugate-linear in each argument of the left factor. The fork branches from leanprover-community/mathlib4 at commit e560e3ad on Lean toolchain v4.30.0-rc1.

4. A framework for reasoning about faithfulness failures in physics formalization. The paper catalogs ways a formal statement can compile and be provable while being physically vacuous or weaker than the source text, and documents two such defects in existing quantum-information benchmarks (Lean-QIT-Bench and Lean-QuantumAlg-Bench, 76 tasks).

Main Findings

• Deterministic, leakage-resistant grading. The Lean kernel checks that the submitted proof compiles, that no sorry appears in it or in any declaration it depends on, and that no new axioms are introduced. Reference proofs for all 1,019 tasks exist but are withheld to keep solutions out of LLM training corpora.

• Broad difficulty spread. Proof length estimates, assigned from the number of declarations a reference proof needs beyond the benchmark library, give 158 tasks (15.5%) "very small", 324 (31.8%) "small", 280 (27.5%) "moderate", 190 (18.6%) "large", and 67 (6.6%) "very large". The largest reference proof introduced more than 450 declarations beyond the benchmark library.

• Some textbook exercises exceed Mathlib. Exercise 9.9 asks for a fixed point of every quantum channel and points to Schauder's theorem; neither Schauder's nor Brouwer's theorem is in Mathlib, so the reference proof instead uses linearity of the channel and a mean-ergodic averaging argument on the compact convex set of density operators.

• High reuse across the library. For the median item in the solution library, 84% of the Lean declarations in its dependency closure are also used by at least one other item. Each Pauli matrix is used by well over a hundred items, as many as 159.

• Tasks depend on each other. 387 of the 1,019 tasks were proved by invoking at least one other task, which motivates two evaluation regimes: an independent regime (each task solved alone) and a dependency-order regime (prerequisite tasks completed first). Chapter-to-chapter dependencies are close to lower-triangular, mirroring the book's pedagogical ordering.

• Chapter coverage is uneven. Chapters 1 (overview) and 3 (classical computation) contribute no items; chapters 7 (physical realization) and 10 (error correction) are densest in tasks per item.

• Not a complete formalization of the book. Of 687 items extracted, 505 were formalized and 479 received benchmark tasks. The remaining 26 were excluded because the item already exists in upstream Mathlib, its proof is needed for another task's statement to compile, it is a definition with no proof to synthesize, it duplicates another item, or it was removed manually for quality. Essay prompts, graph plotting, intuitive arguments, numerical computations, research problems, and infinite-dimensional statements were excluded from the outset.

• Documented defects in prior benchmarks. In a Lean-QIT-Bench task on first-order Lie-Trotter global error scaling, the quantifier order allows the constant K to depend on m, making the statement trivially true; in a phase-estimation task, the circuit is never constructed and its action on an eigenvector is assumed as a hypothesis, so the task follows by linearity. Neither error is caught by the Lean kernel.

Methodology in Plain English

The authors took a standard graduate textbook and identified every numbered item that could be phrased as a rigorous mathematical statement: theorems, problems, exercises, and examples. They built a Lean library of finite-dimensional quantum mechanics on top of a modified copy of Mathlib, then wrote each textbook claim as a Lean theorem statement with the proof removed. Those statements are the benchmark tasks.

To make grading fair, they kept a private "solution library" containing a proof of every task, so every task is known to be solvable. Each task was tagged with a proof-length estimate derived from how many helper declarations its reference proof needed beyond the released library. They also recorded which tasks call which other tasks, producing a dependency ledger that allows the benchmark to be run either task-by-task or in textbook order.

One technical obstacle required changing Mathlib itself: Mathlib's MultilinearMap is linear over a single ring in each argument, which is not general enough to express the inner product on systems composed of several registers. The authors generalized it to a multi-semi-linear map, recovering the original behavior by setting the ring homomorphism to the identity. The same refactor is an open Mathlib pull request (#42534).

Finally, the paper reasons carefully about what the kernel cannot check. A proof assistant verifies logical consistency, not that a statement means what the textbook meant. The authors illustrate this with a toy example where "distance traveled" is defined as ½at² and the theorem then proved by rfl—formally correct, physically vacuous—and argue that high interdependency between declarations constrains, though does not eliminate, such errors.

Why This Matters

Impact on research. Formalization gives physicists machine-checked rigor traceable to first principles, and the paper cites cases where this paid off: formalizing stability conditions of the two-Higgs-doublet potential exposed an error in a widely cited paper, and a machine-verified proof settled an open conjecture in quantum optimization. AxQM supplies the first standardized yardstick for measuring whether AI systems can do this kind of work in quantum information, replacing anecdotal claims with a kernel-checked score.

Potential applications:

• Verified quantum software and compilers: circuit decompositions, universal gate sets, and the quantum Fourier transform are all benchmark topics, and machine-checked versions of these results could underpin certified compilation.
• Certified error-correction and fault-tolerance arguments: stabilizer codes and fault tolerance are among the densest chapters in the benchmark, and these are exactly the claims where a hidden gap is costly.
• Trustworthy AI for theoretical physics: the benchmark separates genuine proof search from plausible-sounding prose, giving labs a way to test whether a model's physics reasoning is actually sound.
• Physics education and textbook auditing: because each task is tied to a specific numbered exercise, the benchmark effectively tests whether a model could complete a course based on Nielsen and Chuang, and it surfaces places where textbook arguments need results absent from Mathlib.

Industry relevance. The benchmark matters directly to AI companies building Lean provers and autoformalization pipelines, to quantum computing firms that want verified rather than merely tested design claims, and to the formal-methods community: it demonstrates that a domain-specific library plus a forked dependency can support a thousand-task benchmark, and it models how to release such a benchmark without leaking solutions into training data.

Future Directions

• Rebasing off the fork. If Mathlib pull request #42534 (the multi-semi-linear MultilinearMap refactor) is accepted, the benchmark can move to a newer pinned Mathlib and drop the fork entirely.
• Community faithfulness audits. The kernel cannot detect vacuous or weakened statements, so the authors explicitly invite physicists and Lean experts to inspect the formal statements against the book, with corrections folded into periodic updates.
• Dual-regime evaluation. The recorded dependency ledger enables comparing models under the independent regime versus the dependency-order regime; how much the ordering helps, and which models benefit most, is left to future benchmarking.
• Extending beyond finite dimensions. Infinite-dimensional systems and unbounded operators are deliberately out of scope; a broader library covering functional-analytic quantum mechanics, and formalizations of other physics textbooks, would test whether the approach generalizes beyond this one text.

Target Audience

Researchers in AI-for-mathematics and automated theorem proving who need physics-domain benchmarks; Lean users and formalization engineers interested in the design of domain libraries and dependency analysis; quantum信息 theorists who want machine-checked versions of standard results; and physicists curious about what formal verification can and cannot certify about their own reasoning. Readers without exposure to proof assistants will find the conceptual sections accessible, but the technical discussion of the Mathlib fork and the failure-mode examples assumes some familiarity with dependent type theory.

Authors’ abstract

Formalizing mathematics in a proof assistant, where a machine checks every definition, statement and proof, has set a new standard of rigor. Large language models are now capable of formalizing autonomously, even at the scale of whole textbooks. We bring this standard of rigor to physics, where theoretical arguments carry idealizations that are rarely stated fully, and any logical gaps could have a cascading effect on interdependent results. Recognizing the need to evaluate autoformalization systems for physics, we release AxQM, 1,019 kernel-checkable proof-synthesis tasks over 479 items drawn from the textbook Quantum Computation and Quantum Information by Nielsen and Chuang. The tasks are stated in a custom Lean library of finite-dimensional quantum mechanics. By task count, it is the largest proof-synthesis benchmark in physics by a factor of four. AxQM is derived from a near-complete formalization of the formal portions of the textbook, so every task is guaranteed a solution, which we keep private. Grading of the benchmark is done deterministically by the Lean kernel, which checks that the proof compiles, that no sorry appears in it or in any declaration it depends on, and that it introduces no new axioms.