Quantum Error Correction in Lean

1 Introduction

This is the blueprint for QECLean, a formalization of the stabilizer formalism for quantum error correction in Lean 4 and Mathlib.

A blueprint is a map of a formalization: informal mathematical exposition, one node per definition or theorem, wired into a dependency graph that shows how the results rest on one another and how much of the plan is already formal. Here every node is already formal — the library is complete and sorry-free — so the graph is best read as a guide to the architecture rather than as a to-do list.

1.1 What is proved

Two results anchor the development.

  • The toric family. For every \(L \ge 2\), the \(L \times L\) toric code is verified as an \([[2L^2, 2, L]]\) stabilizer code: the distance is exactly \(L\), not merely bounded below by it (theorem 70).

  • The gross code. IBM’s \([[144,12,12]]\) bivariate-bicycle code — the flagship qLDPC code of Bravyi et al. — is verified with distance exactly \(12\), unconditionally (theorem 79).

Alongside these sit the rotated surface family, the repetition codes, the iceberg family, and the small named codes: Steane’s \([[7,1,3]]\), Shor’s \([[9,1,3]]\), the perfect \([[5,1,3]]\) code, and the \([[4,2,2]]\) detection code (chapter 10).

1.2 The axiom discipline

Everything on the main branch depends on exactly Mathlib’s three standard axioms — propext, Classical.choice, Quot.sound — and nothing else. In particular there is no native_decide, which would replace a kernel check by a compiler-trust axiom, and no sorry. An input that cannot yet be proved is carried as a named hypothesis on the theorem, where it is visible in the statement rather than hidden in the axiom set. This is enforced in CI, so a violation fails the build rather than landing quietly.

The discipline is not free. The gross code distance proof was originally carried by 135 native_decide leaves and had to be converted to kernel-checkable form: packed natural-number tables instead of array lookups, quantifier bridges so the kernel enumerates concrete lambdas, sparse rewrites in place of large finite sums, and Gaussian-style certificates where a sweep would otherwise be needed.

1.3 Reading the graph

An edge \(A \to B\) in the dependency graph means that \(B\) is the nearest blueprint ancestor of \(A\): LeanArchitect walks the type and the proof term of each annotated declaration and stops as soon as it reaches another annotated declaration. The edges are therefore read off the real proof terms rather than maintained by hand, and a node that a proof genuinely stopped needing loses its edge as soon as the proof changes.