Source-linked AI summary
AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics
Weichen Winston Yin, Jacob M. Taylor, Dirk R. Englund, Frank H. L. Koppens
TL;DR
Physics rarely states its assumptions with mathematical rigor, motivating machine-checked formalization and evaluation of autonomous proof synthesis. AxQM applies this approach to a textbook-scale formalization of quantum information in Lean, while retaining expert review as necessary for physical faithfulness.
Problem
Physics contains assumptions and hand-waving that are rarely expressed at mathematical rigor, motivating machine-checked formalization and evaluation of autonomous formalization.
Method
AxQM formalizes the rigorous mathematical portions of Nielsen and Chuang’s textbook in a Lean library for finite-dimensional quantum mechanics, with 479 benchmarked items.
Results
AxQM provides a textbook-scale physics formalization and benchmark, with 84% of dependency-closure declarations reused by another median item.
Takeaways & Limitations
AxQM is intended as a baseline for evaluating proof synthesis in physics and for measuring whether models can complete a course based on a foundational quantum-information textbook.
Takeaways & Limitations
The Lean kernel checks logical consistency but cannot ensure that formal statements faithfully capture physically meaningful textbook claims, so expert review remains necessary.
Abstract
from arXiv · showhide
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.
1 Introduction
Formalization brings machine-checked rigor to physics, where assumptions and informal reasoning can leave physical arguments under-specified. AxQM applies this approach to a textbook-scale formalization of finite-dimensional quantum information.
- Lean 4 accepts definitions, statements, and proofs only after checking them with a small trusted kernel.
- Physics formalization can expose errors and support machine-verified results, despite the field’s frequent reliance on unstated assumptions and hand-waving.
- A self-consistent scaffold of axioms and definitions is necessary for lemmas and theorems to build reliably.
- AxQM releases a Lean 4 benchmark built from the exercises and formal content of Nielsen and Chuang’s quantum-information textbook.
- The benchmark is restricted to finite-dimensional Hilbert spaces, excluding infinite-dimensional systems and unbounded operators.
2 The Benchmark
AxQM is a large, textbook-derived benchmark of Lean proof-synthesis tasks spanning quantum information topics and difficulty levels. Its kernel-checkable structure supports deterministic evaluation, while shared dependencies provide structural evidence about the underlying library without guaranteeing physical correctness.
- 1,019 proof-synthesis tasks cover 479 textbook items across quantum-information topics including density operators, algorithms, channels, error correction, and entropy.Each item can generate one or more Lean theorem statements.
- The reference solutions range from one-line Pauli-matrix identities to proofs requiring results outside Mathlib, including an averaging argument for a quantum-channel fixed point.
- The benchmark’s census of one textbook differs from sparse multi-source samples by presenting tasks inside a custom quantum-physics library.
- The released benchmark compiles under Lean grading that rejects sorry-dependent proofs and newly added axioms, while omitting the private proof infrastructure.
- The median item shares 84% of its dependency closure with another item, and individual Pauli matrices are used by as many as 159 items.These reuse patterns constrain, but do not guarantee, semantic correctness of the library.
- 387 of 1,019 tasks invoke at least one other task, enabling independent and dependency-order evaluation regimes.
- AxQM is 4.1 times the size of the 250-instance PhysLeanData evaluation set and is described as the largest physics proof-synthesis benchmark to date.
- Expert review remains necessary because Lean can verify a vacuous or physically weaker statement that still compiles and is provable.
3 Forking Mathlib
AxQM forks Mathlib to support the multilinear structure required by finite-dimensional quantum mechanics on multi-register systems. The change generalizes multilinear maps while preserving the original construction as a special case.
- The fork generalizes Mathlib’s multilinear maps from linearity over one ring to multi-semilinearity over ring homomorphisms.
- The original Mathlib formulation is recovered by choosing the ring homomorphism to be the identity.
- This generalization is needed to define inner products on n-ary tensor products, where the left factor is conjugate-linear in each argument.
- The refactor lets multi-party-register benchmark items use Mathlib’s trusted InnerProductSpace machinery.
- The change is the n-ary analogue of an existing semilinear-map construction and was under review as a Mathlib pull request.
4 Failure modes in formalizing physics
Proof assistants can verify formal deductions but cannot ensure that formal statements faithfully capture the intended physics. AxQM discusses definition errors, weakened hypotheses, omitted algorithms, and the need for expert review.
- Formal statements can be provable while meaning something different from the intended physical or mathematical claim.A statement may encode incorrectly defined objects yet remain kernel-checkable.
- A formalization can become vacuous when the conclusion is defined directly and then proved by reflexivity.The distanceTraveled example compiles without sorry or new axioms while merely defining the quantity it proves.
- Faithful physical formalization requires modeling objects with hypotheses and deriving the claimed result, a gap the Lean kernel cannot detect.The trajectory example requires differential constraints and initial conditions before proving the quadratic distance law.
- Benchmark statements can weaken claims by moving critical logical steps into hypotheses or by omitting the algorithm being analyzed.Examples include an asymptotic bound with a quantifier-order error and phase estimation whose circuit action is assumed rather than constructed.
- AxQM minimizes such defects, but evaluating physical correctness and faithfulness still requires broader review by physicists and Lean experts.The Lean kernel checks formal consistency, not whether the formal statement matches the intended physics.
5 Discussion
The discussion distinguishes rigorous derivations from physical assumptions and modeling choices that proof assistants cannot validate. AxQM formalizes the textbook’s mathematical portion while defining a deliberately bounded benchmark scope.
- Physics combines rigorous mathematical derivations with physical assumptions, approximations, and dictionary entries connecting models to measured quantities.The BCS example separates effective attraction and mean-field restriction from later derivations of the gap equation and transition temperature.
- AxQM treats quantum-mechanics postulates as primitives, then uses formal statements as dictionary entries whose consequences are checked by the kernel.Faithfulness of the dictionary entries remains subject to expert review because the kernel cannot prevent physically meaningless starting points.
- From 687 extracted textbook items, 505 are formalized and 479 appear in the benchmark after excluding non-mathematical, redundant, upstream, definitional, dependent, or manually removed items.The exclusions mean AxQM is not a complete formalization of every physically meaningful textbook statement.
- AxQM is presented as the first textbook-scale formalization of physics and as a baseline for evaluating proof synthesis in physics.Its source is Nielsen and Chuang’s foundational textbook, including pedagogically easy problems to measure course-level completion.
6 Data and code availability
AxQM is distributed through a GitHub repository containing the benchmark, supporting library, tooling, and documentation; the repository also accepts comments and error reports.
- The repository includes task statements, the finite-dimensional quantum mechanics library, a Mathlib fork, proof-length estimates, dependency data, and grading scripts.Reference proofs for all 1,019 tasks are kept in a separate solution library.
- Comments and error reports can be submitted as GitHub issues, while inquiries and benchmark submissions can be sent to the authors by email.
Competing interests
The paper reports that W.W.Y., D.R.E., and J.M.T. are affiliated with Axiomatic AI, and that F.H.L.K. is a co-founder.
- W.W.Y., D.R.E., and J.M.T. are affiliated with Axiomatic AI, while F.H.L.K. is a co-founder.