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

• URL: http://arxiv.org/abs/2609.05157v1
• Date: Fri, 04 Sep 2026 13:58:19 GMT
• Title: AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics
• Abstract summary: AxQM is the largest proof-synthesis benchmark in physics by a factor of four.<n>By task count, it is the largest proof-synthesis benchmark in physics by a factor of four.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• QBism Logic [0.0]
  QBism interprets quantum theory as a normative discipline for an agent's probability assignments.<n>This paper develops a logical formalization of that picture.
  arXiv  Detail & Related papers  (2026-07-19T10:20:53Z)
• Lean-Quantum: Toward AI-Assisted Formalization of Quantum Information [4.962621441807053]
  We present a Lean 4 library for quantum information, designed as a reusable formal infrastructure for theoretical analysis.<n>We formalize the DPI for the sandwiched Rényi relative entropy for positive semidefinite operators on finite-dimensional quantum systems.<n>The library provides a basis-independent operator-theoretic framework for finite-dimensional quantum mechanics.
  arXiv  Detail & Related papers  (2026-07-06T18:00:00Z)
• Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics [20.90238876313568]
  Large Language Models (LLMs) produce subtle errors that evade human detection.<n>Recent trends indicate that general-purpose LLMs now outperform smaller models explicitly fine-tuned for Lean.<n>We introduce an agentic autoformalization framework powered by general coding LLMs.
  arXiv  Detail & Related papers  (2026-06-30T05:05:03Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate verifiable proofs in formal languages like Lean.<n>We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving.
  arXiv  Detail & Related papers  (2026-06-02T08:16:42Z)
• Lean Atlas: An Integrated Proof Environment for Scalable Human-AI Collaborative Formalization [1.711666249985278]
  We propose a human-in-the-loop approach in which human scientists and AI collaboratively produce formal proofs.<n>We develop Lean Atlas, a Lean 4 tool that visualizes the dependency graph of a Lean 4 project as an interactive web viewer.<n>Core feature, Lean Compass, is an algorithm that, given a selected theorem set, automatically extracts the project-specific nodes.
  arXiv  Detail & Related papers  (2026-03-16T14:19:33Z)
• A Formalization of the Generalized Quantum Stein's Lemma in Lean [0.0]
  We formalize the proof presented inHayashi and Yamasaki (2024) in the Lean interactive theorem prover.<n>This is the most technically demanding theorem in physics with a computer-verified proof to date.
  arXiv  Detail & Related papers  (2025-10-09T17:41:13Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  This work proposes Alchemy, a framework for data synthesis that constructs formal theorems through symbolic mutation.<n>For each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it.<n>As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M.
  arXiv  Detail & Related papers  (2024-10-21T08:04:21Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  We introduce a neuro-symbolic framework for autoformalizing Euclidean geometry. One challenge is that informal proofs rely on diagrams, leaving gaps in texts that are hard to formalize. We provide automatic semantic evaluation for autoformalized theorem statements.
  arXiv  Detail & Related papers  (2024-05-27T14:35:10Z)
• Unifying (Quantum) Statistical and Parametrized (Quantum) Algorithms [65.268245109828]
  We take inspiration from Kearns' SQ oracle and Valiant's weak evaluation oracle. We introduce an extensive yet intuitive framework that yields unconditional lower bounds for learning from evaluation queries.
  arXiv  Detail & Related papers  (2023-10-26T18:23:21Z)
• Simple Tests of Quantumness Also Certify Qubits [69.96668065491183]
  A test of quantumness is a protocol that allows a classical verifier to certify (only) that a prover is not classical. We show that tests of quantumness that follow a certain template, which captures recent proposals such as (Kalai et al., 2022) can in fact do much more. Namely, the same protocols can be used for certifying a qubit, a building-block that stands at the heart of applications such as certifiable randomness and classical delegation of quantum computation.
  arXiv  Detail & Related papers  (2023-03-02T14:18:17Z)
• Noisy Quantum Kernel Machines [58.09028887465797]
  An emerging class of quantum learning machines is that based on the paradigm of quantum kernels. We study how dissipation and decoherence affect their performance. We show that decoherence and dissipation can be seen as an implicit regularization for the quantum kernel machines.
  arXiv  Detail & Related papers  (2022-04-26T09:52:02Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.