New We formalized a quantum mechanics textbook in Lean. Read the post
Axiomatic AI
← Research
4 min read Winston Yin

From AI Dreams to Verifiable Science: Building a Machine-Verified Formal Library of Physics

Our new paper releases AxQM, a benchmark of 1,019 machine-checkable proof tasks drawn from a near-complete Lean formalization of Quantum Computation and Quantum Information by Nielsen and Chuang. Our system read the textbook and produced a verified proof for every labeled statement in it, showing that autonomous formalization can bring the rigor of formal mathematics to physics at textbook scale.

  • formal methods
  • autoformalization
  • benchmark

Artificial intelligence is rapidly becoming an indispensable tool in scientific work. Today, AI systems such as Lemma can derive equations, write simulation code, analyze data, and search the scientific literature — all core parts of pushing forward the frontier of science.

As these systems become more capable, a fundamental question remains: how do we know that their conclusions are correct? For science, “seems good enough” is not enough. Worse, as the amount of AI-generated code and scientific text skyrockets, the human task of reviewing AI outcomes has only become more daunting. This verification gap is a real challenge we must address to enable scientists to accelerate their work.

This problem is one of trust, and it is especially acute in the physical sciences. Physical reasoning often combines exact mathematics with approximations, modeling choices, and implicit assumptions about the system at hand. Surfacing those reliably remains an open challenge for the community.

One point of light: in mathematics, the ability to formally prove statements has led to the creation of novel results that humans can trust, because they can understand the definitions and the proofs are machine checkable with complete rigor. Can we do this beyond mathematics?

In our paper “AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics”, we released an open-source benchmark for the machine learning and physics community we call AxQM. This benchmark is based upon our team’s formalization of all of the exercises and homework problems in Quantum Computation and Quantum Information by Nielsen and Chuang, a standard textbook in the field of quantum computing and information theory. We’ve proven it’s possible, and we believe that others can as well.

At Axiomatic AI, our aim is to bring about a paradigm of AI for science: one in which the logical steps produced by an AI can be independently and automatically verified. The highest standard for verified reasoning can be found in formal mathematics: once definitions, theorem statements, and proof steps are precisely written in a formal language, the correctness of these reasoning steps can be checked mechanically according to a small set of rules. This process of converting fuzzy reasoning into exact machine-checkable reasoning is called formalization.

In terms of the details: we asked our system based on Axiomatic Intelligence (AxI) to read Nielsen and Chuang. Autonomously, it formalized almost the entirety of the mathematics-based physical reasoning in the book into a coherent code library in Lean, a formal language in which reasoning can be machine-checked. It filled in a rigorous proof for every labeled statement in the book — theorems, examples, exercises — and each one has been verified by Lean, with many additional checks by human experts to confirm the autonomous system’s outputs conform not just to the letter of the text, but to the intent implicit in the exercises. To show what this looks like concretely, there is an interactive walkthrough at the end of this post: Exercise 12.22, on entanglement conversion, taken from the textbook statement through to the Lean one, with every name in it clickable for its definition.

As our system worked through the textbook, it solved new problems using the definitions, theorems, and earlier solved problems as building blocks, and these new results were immediately added to the expanding library. The outcome is a textbook-scale body of quantum theory that is not only generated by AI, but also formally connected to its foundations in a machine-checkable way.

The opportunity here is to combine two capabilities that have so far rarely come together at scale in physics: automation and rigor. We imagined a type of AI system that can work through scientific material on its own, rigorously understand every statement and assumption, formally check every reasoning step, and continuously build on what it has already established. Every isolated problem solved translates into an ever expanding, richly interconnected body of verified scientific knowledge.

The broader significance goes beyond quantum information. If autonomous formalization can be scaled to other areas of physics, it could provide a new foundation for scientific AI: one in which models do not merely generate answers, but continuously build structured bodies of knowledge whose assumptions, dependencies, and conclusions can be checked. This would make it possible to trace a new result back to the principles it depends on, identify which downstream results are affected when an assumption changes, and correct errors in reasoning. AxQM is therefore not only a benchmark for theorem proving in physics, but also a first step toward AI systems that can build and extend scientific knowledge while keeping the formal part of their reasoning verifiable.

From the textbook to Lean · Interactive walkthrough

Nielsen & Chuang, Chapter 12

Exercise 12.22 — entanglement conversion by local operations with no classical communication

We believe that the formalization is only as good as a human expert’s understanding of it.

To facilitate this understanding, our AI system prepared the following explanation of one formalized exercise in AxQM. It is our goal to pair every autoformalization with an “auto-informalization,” and to continuously improve the quality of both.

1 · The statement in the textbook

Exercise 12.22: (Entanglement conversion without communication) Suppose Alice and Bob are trying to convert a pure state ∣ψ⟩\ket{\psi} into a pure state ∣φ⟩\ket{\varphi} using local operations only – no classical communication. Show that this is possible if and only if λψ≅λφ⊗x\lambda_\psi \cong \lambda_\varphi \otimes x, where xx is some real vector with non-negative entries summing to 1, and '≅\cong' means that the vectors on the left and the right have identical non-zero entries.

Transcribed from Quantum Computation and Quantum Information, Nielsen & Chuang, p. 577.

2 · The dictionary between the book's notation and Lean

Click a name for the definition
∣ψ⟩,∣φ⟩|\psi\rangle, |\varphi\rangleψ φ : (A ⊗ B) — the input and target bipartite pure states.
ρψ=TrB∣ψ⟩⟨ψ∣\rho_\psi = \mathrm{Tr}_B|\psi\rangle\langle\psi|ψ.. — Alice's reduced density operator, Bob's side traced out.
λψ\lambda_\psithe non-zero spectrum of ρψ\rho_\psi: its eigenvalues, the squared Schmidt coefficients of ∣ψ⟩|\psi\rangle.
≅\cong (“identical non-zero entries”) — a relation stated directly between the two reduced density operators.
x (“some real vector…”)the spectrum of an ancilla state τ : C. Entries non-negative and summing to 1 automatically, because τ\tau is a density operator.
λφ⊗x\lambda_\varphi\otimes xthe spectrum of ρφ⊗τ\rho_\varphi\otimes\tau, formed with .

3 · How to read a Lean statement

Every theorem in the library has one shape. Read the three views left to right: the bare shape, the same slots filled with the physics, then the real Lean statement. The example is the exercise itself, and the colors mean the same thing in all three. This theorem has no assumption. Everything before the colon introduces objects, and the whole exercise sits in the claim, as a biconditional.

1 · The shape 
theorem ⟨name⟩
    ⟨the objects involved⟩ :
    ⟨what is claimed⟩
name  a label, nothing more objects  what the statement is about claim  everything after the last :

Find the last colon. Everything after it is the claim; the rest introduces the objects. A theorem may also carry assumptions, written (h : …) before the colon. This one carries none.

2 · The physics 
theorem “Exercise 12.22”
    given pure states |ψ⟩, |φ⟩ on A ⊗ B :
    |ψ⟩ ⇝ |φ⟩ by local operations, no classical communication
     ⟺  for some ancilla state τ, ρψ ≅ ρφ ⊗ τ
     (the book's λψ ≅ λφ ⊗ x, with x = λτ)

The same shape with the physics filled in. This is the book's sentence, both directions in one claim, and none of it is Lean yet.

3 · The Lean 
theorem ①
    {A : QSystem} {B : QSystem} (ψ φ : PureState (A ⊗ B))② :
    PureState.ConvertibleNoComm ψ φ ↔③
      ∃ (C : QSystem) (τ : State C),④
        ψ.toState.reducedLeft.SameNonzeroSpectrum (φ.toState.reducedLeft.tmul τ)⑤
  1. The name encodes the statement. Read it as ‘convertible-no-comm iff there-exists same-nonzero-spectrum with-tensor’.
  2. The objects: two pure states on the composite system A⊗BA\otimes B, and the systems AA and BB they live on. Nothing else is given — there is no (h : …), so the theorem assumes nothing.
  3. After the final colon, the claim. ↔ reads “if and only if”, so the claim is both directions of the exercise at once. Its left-hand side is the convertibility predicate, built in § 4.
  4. ∃ …, reads “there exist … such that”: some ancilla system CC carrying a state τ\tau. The eigenvalue list of τ\tau is the book's probability vector xx.
  5. The right-hand side. Read the chain left to right, one .step at a time: ψ\psi → its density operator (toState) → Alice's marginal (reducedLeft) → “has the same non-zero spectrum as” → φ\varphi's marginal tensored with τ\tau (tmul). Altogether: ρψ≅ρφ⊗τ\rho_\psi \cong \rho_\varphi \otimes \tau.

ConvertibleNoComm carries the reading of “local operations, no classical communication”. It is built in § 4, steps 1–3.

4 · The Lean statement of the exercise

Nielsen & Chuang's Exercise 12.22 says that Alice and Bob can turn a bipartite pure state ∣ψ⟩|\psi\rangle into ∣φ⟩|\varphi\rangle using local operations alone, with no classical communication, exactly when λψ≅λφ⊗x\lambda_\psi \cong \lambda_\varphi \otimes x for some probability vector xx. Making that a theorem needs a definite operational meaning for "local operations, no communication", and the biconditional stated over it.

Each card states the claim in ordinary notation, then shows the Lean itself.

The reading path
  1. One party's channel — Alice's most general local operation. A definition.
  2. Both parties at once — the two-sided channel. Still a definition.
  3. What ψ⇝φ\psi\rightsquigarrow\varphi means — convertibility: some such pair of channels does the job. The last definition.
  4. The exercise — convertibility iff the spectra match, both directions as one iff. The only claim.

Steps 1–3 build vocabulary; nothing is claimed until step 4. The theorem inherits its meaning from those definitions.

Throughout: AA and BB are Alice's and Bob's systems, and CC, CAC_A, CBC_B the ancillas a party may adjoin.

variable {A B C : }
variable {CA CB : }

steps 1–3What "local operations without communication" is taken to mean

The book's phrase is informal, so these three definitions come first. Each party's operation is written in Stinespring form: adjoin a pure ancilla ∣ω⟩|\omega\rangle, apply a unitary on system-plus-ancilla, discard the ancilla, giving ℰ(⋅)=TrC(U(⋅⊗∣ω⟩⟨ω∣)U†)\mathcal E(\cdot)=\mathrm{Tr}_C\big(U(\cdot\otimes|\omega\rangle\langle\omega|)U^\dagger\big). Bob's acts on the right factor directly. Alice's acts on the left factor AA and is built from the same construction: swap the two factors, dilate on the (now right-hand) AA factor, then swap back. The two act on disjoint factors and neither is conditioned on the other's result, which is what "no communication" means here. The composite is deterministic, pure state to pure state, matching "convert ∣ψ⟩|\psi\rangle into ∣φ⟩|\varphi\rangle". The existential quantifier runs over dilation data (CA,UA,ωA)(C_A,U_A,\omega_A) and (CB,UB,ωB)(C_B,U_B,\omega_B), not over an abstract type of trace-preserving local maps, so faithfulness rests on Stinespring's theorem rather than on the definition itself.

|ψ⟩ on A ⊗ B AB Alice A |ω⟩C A UA A out discard CA Bob B |ω⟩C B UB B out discard CB no channel crosses here |φ⟩ on A ⊗ B
dilatedChannelNoComm: Bob's dilation, then Alice's, on disjoint factors, drawn for the successful conversion the exercise asks about (output ∣φ⟩|\varphi\rangle). Each box is a Stinespring dilation in N&C's Chapter-8 sense, built once in the Chapter-11 file (Alice's is Bob's conjugated with the swap): adjoin a pure ancilla, run one unitary over system-plus-ancilla, discard the ancilla. “No communication” is only that neither box's unitary depends on anything about the other: no measurement or classical bit ever crosses the dashed line.
Hover a phrase for the matching codea bipartite state ρ
step 1 of 4def

Alice's local operation — a dilated channel on her factor

Nothing can be claimed until “local operation” is pinned down, so the section builds it first, starting with one party:

Alice's half of a local operation: ρ↦(ℰA⊗IB)ρ\rho\mapsto(\mathcal E_A\otimes I_B)\rho, with ℰA(⋅)=TrC(U(⋅⊗∣ω⟩⟨ω∣)U†)\mathcal E_A(\cdot)=\mathrm{Tr}_C\big(U(\cdot\otimes|\omega\rangle\langle\omega|)U^\dagger\big). It takes a bipartite state ρ\rho on A⊗BA\otimes B, a unitary UU acting on A⊗CA\otimes C and an ancilla CC prepared in a pure state ∣ω⟩|\omega\rangle, and returns the state after swapping the two factors, running the Chapter-8 dilation on the (now right-hand) A factor, and swapping back.

Lean · verbatim from the file
noncomputable def  (ρ :  (A ⊗ B)) (U :  (A ⊗ C))
    (ω :  C) :  (A ⊗ B) :=
   ( B A)
    (( ( A B) ρ). U ω)
step 2 of 4def

The two-sided operation — both parties act on their own factor

One party's channel exists; now let both act, each on its own factor:

The operation the exercise quantifies over: ρ↦(ℰA⊗IB)(IA⊗ℰB)ρ\rho\mapsto(\mathcal E_A\otimes I_B)(I_A\otimes\mathcal E_B)\rho. Given a bipartite state ρ\rho on A⊗BA\otimes B, Alice's dilation data (UA,∣ωA⟩)(U_A, |\omega_A\rangle) on A⊗CAA\otimes C_A and Bob's (UB,∣ωB⟩)(U_B, |\omega_B\rangle) on B⊗CBB\otimes C_B, it applies Bob's local channel and then Alice's. The two act on disjoint factors, so the order of application is immaterial.

Lean · verbatim from the file
noncomputable def  (ρ :  (A ⊗ B)) (UA :  (A ⊗ CA))
    (UB :  (B ⊗ CB)) (ωA :  CA) (ωB :  CB) :  (A ⊗ B) :=
  (ρ. UB ωB). UA ωA
step 3 of 4def

The convertibility predicate — what “ψ⇝φ\psi\rightsquigarrow\varphi” means

With both channels defined, the conversion target can be named. The exercise is stated over this definition:

ψ⇝φ\psi\rightsquigarrow\varphi holds when there are ancilla systems CA, CB, a unitary UAU_A acting on A⊗CAA\otimes C_A and a unitary UBU_B acting on B⊗CBB\otimes C_B, and pure states ωA,ωB\omega_A, \omega_B for the ancillas to start in, such that running Bob's dilated channel then Alice's carries ∣ψ⟩⟨ψ∣|\psi\rangle\langle\psi| exactly to ∣φ⟩⟨φ∣|\varphi\rangle\langle\varphi|. Each unitary touches one party's side only, and neither depends on the other's outcome.

Lean · verbatim from the file
def  {A B : } (ψ φ :  (A ⊗ B)) : Prop :=
  ∃ (CA : ) (CB : ) (UA :  (A ⊗ CA)) (UB :  (B ⊗ CB))
    (ωA :  CA) (ωB :  CB),
    φ. = ψ.. UA UB ωA ωB

step 4The exercise: convertibility iff λψ≅λφ⊗x\lambda_\psi \cong \lambda_\varphi \otimes x

The book's λψ\lambda_\psi is the list of eigenvalues of the reduced state ρψ=TrB∣ψ⟩⟨ψ∣\rho_\psi=\mathrm{Tr}_B|\psi\rangle\langle\psi|, i.e. the squared Schmidt coefficients of ∣ψ⟩|\psi\rangle, and ≅\cong means "identical non-zero entries" — realised here as a relation directly between the two reduced density operators, comparing their non-zero eigenvalues. The book's probability vector xx appears as the eigenvalue list of an ancilla density operator τ\tau, so its entries are automatically non-negative and sum to one, and λφ⊗x\lambda_\varphi\otimes x appears as the spectrum of ρφ⊗τ\rho_\varphi\otimes\tau.

step 4 of 4theorem

The exercise: convertibility    ⟺  \iff  λψ≅λφ⊗x\lambda_\psi \cong \lambda_\varphi \otimes x

The exercise itself:

For any two bipartite pure states ∣ψ⟩,∣φ⟩|\psi\rangle, |\varphi\rangle: ψ⇝φ\psi\rightsquigarrow\varphi if and only if there is an ancilla state τ\tau with ρψ≅ρφ⊗τ\rho_\psi \cong \rho_\varphi \otimes \tau — the book's λψ≅λφ⊗x\lambda_\psi \cong \lambda_\varphi \otimes x, with xx the spectrum of τ\tau.

sorry is Lean's placeholder for a missing proof. It stands here on purpose: the statement is what the benchmark asks a model to prove, so the proof is removed. The real one lives in a solution library we keep private.

Lean · verbatim from the file
theorem 
    {A : } {B : } (ψ φ :  (A ⊗ B)) :
     ψ φ ↔
      ∃ (C : ) (τ :  C),
        ψ... (φ... τ) := sorry

5 · The statement, as a graph

unitary Uapply U to ρidentity evolutionproduct U ⊗ Vpure state |ψ⟩ConvertibleNoCommthe exercise (iff)|ψ⟩⟨ψ| density opsystemsystem isomorphismswap A⊗B ≃ B⊗Aregroup (A⊗B)⊗Ccomposite A ⊗ Bstate ρsame non-zero spectrum ≅relabel a statetwo-sided channelAlice's channelBob's channel (Ch 11)spectrum λ(ρ)partial trace Tr_Bproduct ρ ⊗ τ
the exercise definitions of this exercise (+ Ch 11) library definitions basic structures
The exercise and the 21 notions its statement rests on, 78 references in all, extracted from the kernel-checked development. Convertibility unfolds to the two-sided channel, the dilations, and unitaries on relabelled composites; the spectral side unfolds through the partial trace to the spectrum. Everything bottoms out in the five basic structures: system, state, pure state, unitary, isomorphism.