The Quantum toolkit exports circuits to Lean 4 so correctness claims about a program become machine-checkable theorems. The machinery has been in place for a while, but until recently a handful of the exported obligations were still sorry-stubs — they typechecked but weren't actually proven. This post covers the recent pass of closures.
What Gets Exported
Each circuit emitted by the compiler carries annotations: Assert, Prove, Ensures, Requires, Invariant, ResourceBound. The Lean 4 exporter turns the circuit plus its annotations into a file with:
- the circuit as a term-level definition over
Qubit n, - denotational semantics via
denoteinto a unitary matrix, - one
theoremper annotation, stated againstdenoteor a resource predicate.
For a while some of those theorems were by sorry. They compiled, CI passed, but nothing was actually proved.
QFT and Roots of Unity
The QFT obligation that lagged longest was dft_unitary: showing the DFT matrix built from primitive $n$-th roots of unity is unitary. The proof reduces to the standard orthogonality identity
$$\sum_{k=0}^{n-1} \omega^{jk} \overline{\omega^{lk}} = n \cdot \delta_{j,l}$$
for $\omega = e^{2\pi i / n}$. Mathlib v4.29 has most of the algebraic pieces — Complex.exp, Finset.geom_series_def, Complex.norm_exp_ofReal_mul_I — but the sum-of-geometric-series identity over complex roots of unity wasn't in a directly usable shape. The closure is mostly packaging: show the non-diagonal case is a geometric series with common ratio $\omega^{j-l} \ne 1$, invoke Finset.geom_sum_eq, and simplify using $\omega^n = 1$. The diagonal case is a trivial sum of ones.
There's still one residual packaging step — wiring the orthogonality lemma through the matrix product M Mᴴ — but the mathematical content is closed.
BlockEncoding and ECC
The block-encoding theorems were placeholders of the form theorem foo : Prop := sorry. The closure promoted them to proper types stating the actual encoding invariant: given a block encoding $(A, \alpha, \epsilon)$, the top-left block of $U$ approximates $A/\alpha$ up to $\epsilon$. The theorem statement is now load-bearing — future passes that synthesize block encodings can cite it.
For the repetition code, rep3_encode was a placeholder. It's now defined as denote [CX(0,1); CX(0,2)], which is what the encoder emits. The proof that encode-then-decode restores the logical state reduces to computing the product of two CNOTs, which Lean can handle by decide on the small matrix.
QPE and Grover
The existential goals — "there exists a choice of parameters under which the algorithm succeeds" — closed via explicit witnesses. For QPE, the witness is $\phi = k/2^n$ for an integer $k$; for Grover, it's the Grover angle $\theta = \arcsin(1/\sqrt{N})$. The hard part isn't the witness, it's the periodicity lemma omega_periodic, which states that phases wrap consistently under QFT evaluation. That one fell out once the roots-of-unity machinery above was in place.
The Scripts
Mathlib is big, and downloading it from scratch in CI is slow. There's a small mathlib-downloader script that caches the compiled oleans, and an opt-in CI stage that runs the Lean proofs only when the lean4 path changes. The default CI remains Rust-only and stays fast.
What's Next
The Aria → Lean 4 extraction pipeline is up: annotations in Aria source (the strategy DSL reused for quantum circuit specs) lower to Lean theorem statements. The next tranche is proving the TOHPE kernel-search optimizer preserves circuit semantics — the optimizer runs Gaussian elimination over $\mathbb{F}_2$ and the correctness claim is that the resulting phase polynomial is equivalent. The mathlib support for $\mathbb{F}_2$ linear algebra is good, so the obstacles are packaging rather than novel mathematics.
The Quantum toolkit is closed source and currently has no plans to open. The underlying runtime is open source at github.com/Anzaetek/omega-functions-public. Lean 4 / Rocq exporters live on the closed-source side; the emitted proof artifacts themselves can be published per-circuit when a customer wants independent verification.