← All insights

From a circuit you can read to a theorem a machine has checked

Aria Language →aria · lean4 · proofs · formal-methods

Aria can export a circuit to Lean 4, so a claim about a program becomes a theorem a machine can check. The proof tree ships inside the Aria repository at proofs/lean4/QuantumProofs, and it is sorry-free: nothing in it is assumed.

What gets exported

Circuits can carry annotations: Assert, Prove, Ensures, Requires, Invariant, ResourceBound. aria export --lean turns the circuit and its annotations into a Lean file with:

  • the circuit as a definition over n qubits,
  • its meaning as a unitary matrix, via denote,
  • one theorem per annotation.

For the recognized circuits (Bell, GHZ, QFT, QPE, Grover) the exported file closes against the shared tree. For example Generated/GateModel/Bell_Spec.lean is exactly what aria export --gate-model emits for a Bell pair, and it proves.

The proofs that took longest

For a while a few of those theorems were stubs: they compiled, but nothing was proved. Closing them was mostly packaging, not new mathematics.

QFT is unitary. The quantum Fourier transform is a matrix built from n-th roots of unity, and qft_correct in QFT.lean says the circuit computes exactly that matrix. Unitarity comes down to one identity: summing ω^(jk) times the conjugate of ω^(lk) over k gives n when j = l and zero otherwise. Off the diagonal it is a geometric series whose ratio is not 1, so it sums to zero; on the diagonal it is n ones.

Block encodings. The block-encoding theorems used to be placeholders. They now state the real invariant: the top-left block of the unitary approximates A/α to within ε, so later passes that build block encodings have something concrete to cite.

QPE and Grover. Both needed a witness: a phase of the form k/2^n for phase estimation, and the Grover angle arcsin(1/√N) for search. The witnesses were easy; the lemma that phases wrap consistently under the QFT was the real work, and it fell out of the roots-of-unity identity above.

What else is in the tree

Beyond the exported circuits, the same tree formalizes pieces of the runtime itself: gate matrices and adjoints, reset semantics, the stabilizer model, MPS truncation error, HHL and QSVT structure, and the forward and converse theorems of quantum signal processing, which we wrote about separately.

Try it

$ aria export examples/aria/bell.aria --circuit Bell --lean
$ cd proofs/lean4 && lake build

The first command writes the Lean file; the second checks it against the tree.