AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics
Authors: Weichen Winston Yin, Jacob M. Taylor, Dirk R. Englund, Frank H. L. Koppens
Organizations: Axiomatic AI. · Massachusetts Institute of Technology (MIT) · Institut de Ciències Fotòniques (ICFO). · Institució Catalana de Recerca i Estudis Avançats (ICREA).
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.
Figures & tables
Figure 1: Coverage: items and tasks by chapter of Nielsen and Chuang. Items refer to explicitly numbered items in the book: theorems, problems, exercises, and examples. Tasks are individual Lean theorem statements that capture all or part of an item. Each item may have multiple tasks. Chapters 1 (overview) and 3 (classical computation) contribute no items to the benchmark. Chapters 7 (physical realization) and 10 (error correction) are the densest in tasks per item.
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%
Table 1: Proof length estimates for the 1,019 benchmark tasks. The band is assigned from the number of declarations a task’s reference proof needs beyond the released benchmark library. It estimates the length of a reference proof, not how hard a task is for a human or a model to solve.
Figure 3: Direct dependencies between tasks, aggregated by chapter, measured on the full solution library. For example, there are 15 instances of tasks in chapter 7 directly depending on tasks in chapter 4. The matrix is close to lower-triangular, which reflects the pedagogical structure of the book, where later chapters build upon earlier chapters.
We introduce MerLean, a fully automated agentic framework for autoformalization in quantum computation. MerLean extracts mathematical statements from \LaTeX{} source files, formalizes them into verified Lean~4 code built on Mathlib, and translates the result back into human-readable \LaTeX{} for semantic review. We evaluate MerLean on three theoretical quantum computing papers producing 2,050 Lean declarations from 114 statements in total. MerLean achieves end-to-end formalization on all three papers, reducing the verification burden to only the newly introduced definitions and axioms. Our results demonstrate that agentic autoformalization can scale to frontier research, offering both a practical tool for machine-verified peer review and a scalable engine for mining high-quality synthetic data to train future reasoning models. Our approach can also be generalized to any other rigorous research in mathematics and theoretical physics.
Yuanjie Ren, Jinzheng Li, Yidi Qi
Massachusetts Institute of Technology Cambridge, MA 02139 · Northeastern University Boston, MA 02115
Formalising informal mathematical reasoning into formally verifiable code is a significant challenge for large language models. In scientific fields such as physics, domain-specific machinery (e.g. Dirac notation, vector calculus) imposes additional formalisation challenges that modern LLMs and agentic approaches have yet to tackle. To aid autoformalisation in scientific domains, we present FormalScience; a domain-agnostic human-in-the-loop agentic pipeline that enables a single domain expert (without deep formal language experience) to produce syntactically correct and semantically aligned formal proofs of informal reasoning for low economic cost. Applying FormalScience to physics, we construct FormalPhysics, a dataset of 200 university-level (LaTeX) physics problems and solutions (primarily quantum mechanics and electromagnetism), along with their Lean4 formal representations. Compared to existing formal math benchmarks, FormalPhysics achieves perfect formal validity and exhibits greater statement complexity. We evaluate open-source models and proprietary systems on a statement autoformalisation task on our dataset via zero-shot prompting, self-refinement with error feedback, and a novel multi-stage agentic approach, and explore autoformalisation limitations in modern LLM-based approaches. We provide the first systematic characterisation of semantic drift in physics autoformalisation in terms of concepts such as notational collapse and abstraction elevation which reveals what formal language verifies when full semantic preservation is unattainable. We release the codebase together with an interactive UI-based FormalScience system which facilitates autoformalisation and theorem proving in scientific domains beyond physics.https://github.com/jmeadows17/formal-science
Jordan Meadows, Lan Zhang, Andre Freitas
Independent Researcher · University of Manchester, UK · Idiap Research Institute, Switzerland +1
We present FormalProofBench, a private benchmark designed to evaluate whether AI models can produce formally verified mathematical proofs at the graduate level. Each task pairs a natural-language problem with a Lean~4 formal statement, and a model must output a Lean proof accepted by the Lean 4 checker. FormalProofBench targets advanced undergraduate and graduate mathematics, with problems drawn from qualifying exams and standard textbooks across topics including analysis, algebra, probability, and logic. We evaluate a range of frontier models with an agentic harness, and find that the best-performing foundation model achieves 33.5% accuracy, with performance dropping rapidly after that. In addition to the accuracy numbers, we also provide empirical analysis of tool-use, failure modes, cost and latency, thereby providing a thorough evaluation of the formal-theorem proving abilities of frontier models.
Nikil Ravi, Kexing Ying, Vasilii Nesterov +5
Vals AI · École Polytechnique Fédérale de Lausanne (EPFL) · Moscow Institute of Physics and Technology +2