QEC formalization pipeline
Catalog-driven Lean 4 formalization of quantum error-correcting codes. Last scored 2026-07-18.
New here? What this dashboard tracks
This is a progress tracker for a
Lean 4 formalization of
stabilizer-formalism quantum error-correcting codes (QEC). The codes
themselves come from the
Error Correction Zoo —
a community-maintained catalog of ~267 quantum codes.
Formalization here means proving every claim about a code —
parameters [[n,k,d]], stabilizer generators, logical operators,
code distance — inside a proof assistant, so the end artifact is
machine-checked mathematics rather than an informal write-up.
The pipeline scores every catalog entry on six axes (reuse: how directly existing infrastructure applies; canonicality: textbook/syllabus weight; hardware: appearance in published hardware demos; tractability: whether a clean distance proof is known; prerequisites: how much missing infrastructure stands in the way; effort: cheapness to formalize). Each axis is graded 0–10 and combined into a single composite score:
The composite sorts each code into one of four tracks:
engineering (known proofs — let the agents grind) ·
moonshot (novel research — distance proof is the open problem) ·
defer (blocked on missing infrastructure) ·
skip (not worth pursuing in this repo).
Claude Code agents draft Lean skeletons and close sorry
markers; a human reviews at two gates — spec review
(catch wrong theorem statements before proof effort) and
PR review (final code).
Reading this dashboard: Overview — counts, in-flight, queue head · Queue — all 267 codes, sortable · Research — moonshots; failures are first-class outputs
Deeper reading: docs/pipeline.md (architecture) · docs/pipeline-usage.md (operator's manual)
Engineering queue head top of queue, not yet done
| Code | Name | Score | Axes |
|---|---|---|---|
| bb72 | [[72,12,6]] BB6 code [[72,12,6]] |
8.65 | |
| stab_8_3_3 | [[8, 3, 3]] Eight-qubit Gottesman code [[8,3,3]] |
8.30 | |
| xzzx | XZZX surface code | 8.25 | |
| stab_8_2_3 | [[8,2,3]] Hermitian code [[8,2,3]] |
8.00 | |
| stab_10_2_3 | [[10,2,3]] binarized Galois-qudit code [[10,2,3]] |
7.95 | |
| stab_9_3_3 | [[9,3,3]] Quadric code [[9,3,3]] |
7.95 | |
| stab_10_1_2 | [[10,1,2]] Vasmer-Kubica code [[10,1,2]] |
7.90 | |
| stab_12_2_2 | [[12,2,2]] CSS code [[12,2,2]] |
7.90 |
Moonshots research-track candidates
| Code | Score | Status |
|---|---|---|
| bb288 | 6.15 | not started |
| honeycomb_floquet | 5.20 | not started |
| kitaev_honeycomb | 5.05 | not started |
Recent activity latest commits touching pipeline/, catalog/, or (in QECLean) QEC/Stabilizer/Codes/
- 2026-10-13 00d2954 Merge pull request #32 from Stavan-Jain/codex/bb-growing-fom-research
- 2026-10-07 e88ec48 Audit research, document recovery, and fix degenerate census cases
- 2026-09-29 87a4cd1 refactor: route Gross distance through generic doubling
- 2026-09-15 fc6e7cf refactor(wip): decide route for literal small codes; drop Z/X set scaffolding
- 2026-09-14 12156e6 Link companion draft PRs and published Lean sources
- 2026-09-13 3158e84 Document proved weight-six BB family and Lean validation
- 2026-09-11 748f15c refactor: drop redundant `g ∉ S` conjunct from RepresentsNontrivialCoset
- 2026-09-11 aba3752 feat: decide generator conditions; implicit args on independence lemma
See docs/pipeline.md for the architectural overview, and docs/pipeline-usage.md for the task-oriented recipes.