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
quant-ph · cs.AI · cs.LO
Quick verdict
Releases 1,019 kernel-graded Lean proof tasks from Nielsen–Chuang, the largest physics benchmark; sound design, but no model results yet.
Summary
The authors release AxQM, a Lean 4 benchmark of 1,019 kernel-checkable proof-synthesis tasks spanning 479 numbered items from Nielsen and Chuang's Quantum Computation and Quantum Information, restricted to finite-dimensional Hilbert spaces. Tasks are stated in a custom quantum-mechanics library of 3,519 declarations built on a fork of Mathlib (commit e560e3ad, Lean v4.30.0-rc1) in which MultilinearMap is generalized to multi-semilinear maps so inner products can be defined on n-ary tensor products. Reference proofs (10,560 declarations) are withheld to avoid training contamination, which also guarantees every task is solvable; grading is deterministic: compiled proof, no sorry in dependencies, no new axioms. At 4.1 times the 250-instance PhysLeanData held-out split, the authors claim the largest physics proof-synthesis benchmark to date. Each task carries a five-band proof-length estimate derived from reference-proof declaration counts, and a published dependency ledger shows 387 tasks invoke other tasks, enabling independent or dependency-order evaluation. The paper candidly analyzes semantic failure modes the kernel cannot detect and critiques quantifier-ordering and hypothesis-circumvention defects in earlier quantum benchmarks. Main limitations: no evaluation of any LLM or prover on AxQM is reported; faithfulness to the textbook rests on human review rather than machine checking; and the solvability guarantee depends on private, unauditable artifacts.
Review complete
Assessment at a glance
5
risk flags identified
● high 0
● medium 2
● low 3
5 strengths · 5 weaknesses · 5 author questions
AI text signal = Binoculars zero-shot detector score over 20 sampled passages (Fast-DetectGPT co-reported) — absence does not prove human authorship, and a flag does not imply misconduct.
Levels reflect verification complexity — not a quality score. Evolve never rates your paper.
Key claims under review
- AxQM provides 1,019 kernel-checkable Lean 4 proof-synthesis tasks over 479 numbered items of Nielsen and Chuang's textbook, the largest physics proof-synthesis benchmark at 4.1 times the 250-instance PhysLeanData held-out split.
- Every task is guaranteed solvable because the benchmark derives from a near-complete formalization whose reference proofs (10,560 declarations) are withheld to stay out of training corpora.
- Grading is fully deterministic: the Lean kernel checks compilation, absence of sorry in all dependencies, and introduction of no new axioms.
- Formalizing finite-dimensional quantum mechanics required forking Mathlib to generalize MultilinearMap to multi-semilinear maps, enabling inner products on n-ary tensor products; the refactor is under upstream review as PR #42534.
- Kernel acceptance does not certify statement faithfulness; AxQM mitigates via high library interdependency (84% median shared dependency closure) and external human review, while explicitly inviting community audit.
Strengths
Scale claim is substantiated against named comparators
1,019 tasks over 479 items (Fig. 1) versus 76-200 tasks for prior purpose-built physics benchmarks [13, 49, 58] and the 250-instance held-out split of PhysLeanData [59] - a 4.1x margin, with even per-item counting (479) exceeding all predecessors.
Deterministic, contamination-aware evaluation design
Grading checks compilation, absence of sorry in all dependencies, and no new axioms; the private 10,560-declaration solution library simultaneously guarantees solvability and keeps reference proofs out of training corpora, citing contamination-mitigation literature [64, 65].
Candid failure-mode analysis that benefits the whole field
Well-justified Mathlib fork rather than an ad hoc one
Published dependency structure enables two evaluation regimes
Weaknesses
No baseline or evaluation results of any kind
Semantic faithfulness is neither kernel-checkable nor systematically audited
Solvability guarantee rests on unauditable private artifacts
Difficulty metadata is explicitly not difficulty
Fork lock-in and interest alignment
Full Review Report
$1.99 · one-timeUnlock the complete preliminary analysis Evolve produced for this paper.
Report preview
Scope & Claims
AxQM (arXiv:2609.05157) is a dataset/benchmark paper by Axiomatic AI, MIT and ICFO authors. It releases 1,019 Lean 4 proof-synthesis tasks over 479 numbered items (theorems, exercises, examples) from Nielsen and Chuang's *Quantum Computation and Quantum Information*, restricted to finite-dimensional Hilbert spaces; chapters 1 and 3 contribute nothing (Fig. 1). The central claims: (i) largest kernel-checkable proof-synthesis benchmark in physics, at 4.1x the 250-instance held-out split of PhysLeanData [59] and well above the 76-200-task range of predecessors [13, 49, 58]; (ii) every task guaranteed solvable, because the benchmark derives from a near-complete private formalization (10,560 declarations vs. 3,519 released); (iii) deterministic grading via the Lean kernel (compilation, no sorry in dependencies, no new axioms). The item accounting is transparent: 687 items extracted, 505 formalized, 479 benchmarked, with the 26 exclusions itemized under five reasons (§5).
The remaining sections cover Methodology Assessment, Statistical Evidence, Results & Reproducibility, Limitations & Risks, and Verdict & Recommendations.
- All 5 strengths & 5 weaknesses, analyzed in detail
- 5 risk flags with severity, section & reviewer questions
- Methods & statistical evidence assessment
- 5 questions a peer reviewer would ask
- Full six-dimension evaluation report & recommendations
One-time purchase · this paper only
One-time purchase, this paper only. AI-generated preliminary analysis — not peer review.
Frequently asked questions
What is AxQM?
AxQM is a Lean 4 benchmark of 1,019 machine-checkable proof-writing tasks covering 479 numbered theorems, exercises and examples from Nielsen and Chuang's textbook Quantum Computation and Quantum Information, stated in a custom finite-dimensional quantum-mechanics library and graded automatically by the Lean kernel.
How does AxQM compare in size to other physics proof benchmarks?
Prior purpose-built physics proof-synthesis benchmarks had 76 to 200 tasks, and the largest comparable evaluation set is a 250-instance held-out split of PhysLeanData. AxQM's 1,019 tasks make it about four times larger than any of them.
Are the solutions to AxQM tasks public?
No. The reference proofs (about 10,560 Lean declarations) are withheld so they do not leak into LLM training data. The benchmark library, the Mathlib fork, per-task length estimates, the dependency ledger and grading scripts are public on GitHub under Apache 2.0.
Does passing the Lean kernel checker guarantee a task statement is faithful to the textbook?
No. The kernel only verifies that a proof compiles without admissions or new axioms; whether the formal statement actually captures the textbook's claim requires human review. The authors discuss this limitation openly and invite community audit of the statements.
About this review
This is an AI-generated preliminary review by Evolve.Pub, produced from the openly available text of the paper. It is not peer review and does not represent the authors' views. The canonical record of the paper is at the publisher link above.
- Figures 1-3 are extracted as interleaved axis/tick text, so individual values (e.g., the Fig. 3 dependency-matrix entries) are legible but their positional mapping to matrix cells is inferred from reading order.
- Footnote 2's repository identifiers are fused with body text in extraction ('2QudeLeap/Lean-QuantumAlg-Bench...'); the commit hashes b540e86 and 231830d remain legible.
Go deeper on this paper
Wrote a paper? Stress-test it before reviewers do.
Upload your manuscript for the same structured scrutiny — reasoning, statistics, evidence, figures, and reproducibility.