Done · 14 codes formalized

Stabilizer codes with end-to-end mechanized proofs in this repo. Pipeline-era attempts link to their full write-ups (result.md and friends); earlier codes link to their Lean source directly.

Concrete codes

Sorted by code length n ascending.

css_4_1_2 [[4,1,2]]

[[4,1,2]] Leung-Nielsen-Chuang-Yamamoto (LNCY) code

QEC/Stabilizer/Codes/Small/CSS_4_1_2.lean (PR #32, merged 2026-05-23). 505 LoC, 26 sorries closed in two stages. The [[4,1,2]] LNCY code, the unique 4-qubit CSS detection code. Direct instance of existing CSS / Stabiliz…

attempt write-up →

stab_6_2_2 [[6,2,2]]

[[6,2,2]] C_6 code

DONE (merged 2026-05-24, PR #39): formalized in QEC/Stabilizer/Codes/Small/SixQubit_6_2_2.lean (805 LoC, 47 sorries closed), packaged as `stabilizerCodeWithDistance : StabilizerCodeWithDistance 6 2 2`. Knill's C_6 code…

attempt write-up →

stab_6_4_2 [[6,4,2]]

[[6,4,2]] error-detecting code

[[6,4,2]] is the m=3 instance of the parametric iceberg family [[2m, 2m-2, 2]] that QEC/Stabilizer/Codes/Iceberg/N.lean defines for m ≥ 2 (PR #36, merged 2026-05-24)

steane [[7,1,3]]

[[7,1,3]] Steane code

QEC/Stabilizer/Codes/Small/Steane7.lean.

Steane7.lean

shor_nine [[9,1,3]]

[[9,1,3]] Shor code

QEC/Stabilizer/Codes/Small/Shor9.lean.

Shor9.lean

surface-17 [[9,1,3]]

[[9,1,3]] Surface-17 code

explicitly a [[9,1,3]] rotated surface code — the L=3 instance of QEC/Stabilizer/Codes/RotatedSurface/N.lean (with stabilizer-code packaging in RotatedSurfaceCodeNStabilizerCode.lean and distance proof in RotatedSurface…

N.lean

stab_15_7_3 [[15,7,3]]

[[15, 7, 3]] quantum Hamming code

[[15,7,3]] is the r=4 instance of the quantum Hamming family [[2^r-1, 2^r-1-2r, 3]] that QEC/Stabilizer/Codes/Small/QuantumHamming.lean defines parametrically for r ≥ 3

QuantumHamming.lean

gross [[144,12,12]]

[[144,12,12]] gross code

DONE (2026-07-06, bb_lab Phase-A program): d(gross) = 12 proven — unconditional and axiom-clean in Lean (standard three axioms + the native_decide compiler axiom, no sorry). Capstone `grossStabilizerCodeWithDistance : S…

attempt write-up →

Parametric families & abstractions

Codes that span a family (any L, any r) or capture an abstraction rather than a concrete code.

iceberg

[[2m,2m-2,2]] error-detecting code

formalized in QEC/Stabilizer/Codes/Iceberg/N.lean (parametric [[2m, 2m-2, 2]] family, m >= 2) and umbrella at QEC/Stabilizer/Codes/Iceberg.lean (PR #36, merged 2026-05-24). 765 LoC, 24 sorries closed in Stage 4. Direct…

attempt write-up →

quantum_hamming

[[2^r, 2^r-r-2, 3]] Gottesman code

QEC/Stabilizer/Codes/Small/QuantumHamming.lean.

QuantumHamming.lean

quantum_repetition

Quantum repetition code

QEC/Stabilizer/Codes/Repetition/{Three,N}.lean.

Three.lean N.lean

qubit_stabilizer

Qubit stabilizer code

the abstract qubit-stabilizer-code class. Already implemented as the Stabilizer/Core/StabilizerGroup + Stabilizer/Core/StabilizerCode infrastructure in this repo — not a concrete code to be formalized separately

QEC/Stabilizer/Core/

rotated_surface

Rotated surface code

QEC/Stabilizer/Codes/RotatedSurface/*.lean.

QEC/Stabilizer/Codes/RotatedSurface/

toric

Toric code

QEC/Stabilizer/Codes/Toric/CodeN*.lean.

QEC/Stabilizer/Codes/Toric/

See queue for the rest of the catalog, or research for moonshot attempts where the distance proof is the open problem.