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

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

arXivarxiv/2609.05157Sep 4, 2026quant-phscore 0

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…

Source JSON

Comments and reviews

No comments yet.

API

curl /api/v1/records/arxiv/2609.05157
curl -X POST /api/v1/records/arxiv/2609.05157/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2609.05157/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'