pith. sign in

arxiv: 2605.16523 · v1 · pith:DDVWRWY2new · submitted 2026-05-15 · 🪐 quant-ph · cs.LO

End-to-End Formalization of Quantum Error Correction

Mattias Ehatamm , Yi Lee , Xiaodi Wu , Runzhou Tao This is my paper

Pith reviewed 2026-05-20 18:41 UTC · model grok-4.3

classification 🪐 quant-ph cs.LO
keywords quantum error correctionformal verificationstabilizer codesqLDPC codesBivariate Bicycle codesdistance certificationLean proof assistant
0
0 comments X

The pith

Lean formalization yields the first machine-checked distance proofs for industrial quantum error-correcting codes.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops Lean-QEC as the first full formalization of stabilizer-code theory inside the Lean 4 proof assistant. It converts the distance lower-bound condition into a Boolean satisfiability instance through a verified reduction, then solves that instance inside Lean to produce machine-checked certificates. The approach handles codes from the Bivariate Bicycle and Generalized Bicycle families at sizes that matter for hardware, such as the [[90, 8, 10]] and [[70, 6, 9]] codes. A sympathetic reader would care because the distance number directly determines how many errors a code can correct, yet previous values rested on either tiny hand proofs or unverified solvers that leave an unclosed trust gap.

Core claim

Lean-QEC formalizes the linear algebra of qubit states, the Pauli group, stabilizer codes, the binary symplectic representation, classical coding theory, and the CSS and Bivariate Bicycle families. It translates the distance condition into a Boolean satisfiability formula via a verified reduction, then applies a BitVec-flattened encoding and an error-location encoding that reduces variables from n to k⌈log₂ n⌉. These steps produce automatically generated Lean-checked distance proofs for a large range of industrially viable qLDPC codes, including [[90, 8, 10]] and [[70, 6, 9]] BB codes, with the formulation scaling to 144 qubits when run outside the Lean kernel.

What carries the argument

The verified reduction of the distance condition to a Boolean satisfiability formula, supported by BitVec-flattened matrix encoding and error-location encoding that shrinks variable count from n to k⌈log₂ n⌉.

If this is right

  • Distance values for Bivariate Bicycle and Generalized Bicycle qLDPC codes can now be certified by machine-checked proofs rather than unverified solvers.
  • The reusable library is designed to plug into broader Lean-based efforts toward end-to-end verification of fault-tolerant quantum computation.
  • The same pipeline scales to 144 qubits when the satisfiability solving step is performed outside the Lean kernel.
  • Automatically generated Lean-checked proofs become available for a wide range of codes previously limited to non-scaling hand proofs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same reduction technique could be applied to other stabilizer-code families once their linear-algebra definitions are added to the library.
  • Hardware designers could select codes by consulting these verified distance numbers instead of trusting external solver output.
  • Full-stack verification of quantum algorithms might become feasible by composing this library with existing Lean developments for quantum circuits.

Load-bearing premise

The reduction from the distance condition to a Boolean satisfiability formula together with the BitVec and error-location encodings correctly preserves the original mathematical statement inside Lean.

What would settle it

An independent calculation of the minimum weight of a nonzero stabilizer element in the [[90, 8, 10]] code that differs from the weight certified by the Lean proof.

Figures

Figures reproduced from arXiv: 2605.16523 by Mattias Ehatamm, Runzhou Tao, Xiaodi Wu, Yi Lee.

Figure 1
Figure 1. Figure 1: Verification workflow for fault-tolerant quantum programs. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Map of the formalized quantum-error-correction stack. Arrows are machine-checked correspondence [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Tensor product of unfolded Pauli operators [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
read the original abstract

Quantum error-correcting codes (QECCs) sit between noisy quantum hardware and reliable computation, so the code parameters used in practice must be trustworthy. The single number that summarizes a code's strength is its distance, yet certifying a distance lower bound is NP-hard in general, placing it beyond the reach of pen-and-paper proofs as well as direct proof-assistant scripting. As a result, distance values in the literature come either from non-scaling hand proofs, or from unverified solvers that leave a trust gap exactly where the code is supposed to provide a guarantee. We present Lean-QEC, the first Lean 4 formalization of stabilizer-code theory that delivers end-to-end, machine-checked distance certificates at industrial code sizes. Lean-QEC formalizes the linear algebra of qubit states, the Pauli group, stabilizer codes, the binary symplectic representation, classical coding theory, and the CSS and Bivariate Bicycle families. To break the combinatorial barrier, Lean-QEC translates the distance condition into a Boolean satisfiability formula through a verified reduction. The pipeline scales through a BitVec-flattened encoding that replaces Lean's Matrix representation, and an error-location encoding that reduces the variable count from $n$ to $k\lceil \log_2 n\rceil$. With these, we obtain automatically-generated Lean-checked distance proofs for a large range of industrially viable qLDPC codes within the Bivariate Bicycle and Generalized Bicycle families, including [[90, 8, 10]] and [[70, 6, 9]] BB codes, with the formulation scaling up to 144 qubits when performed outside the Lean kernel. The resulting library is reusable and is designed to plug into broader Lean-based efforts toward end-to-end verification of fault-tolerant quantum computation.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript introduces Lean-QEC, the first Lean 4 formalization of stabilizer-code theory (linear algebra of qubit states, Pauli group, binary symplectic representation, classical coding theory, CSS and Bivariate Bicycle families). It translates the distance lower-bound condition (no nontrivial logical operator of weight < d) into a Boolean satisfiability formula via a verified reduction, employing a BitVec-flattened encoding of matrices and an error-location encoding that reduces variables from n to k⌈log₂ n⌉. This yields automatically generated, Lean-checked distance proofs for qLDPC codes in the Bivariate Bicycle and Generalized Bicycle families, including [[90, 8, 10]] and [[70, 6, 9]] BB codes, with the formulation scaling to 144 qubits when performed outside the Lean kernel. The resulting reusable library is positioned for integration into broader Lean-based verification of fault-tolerant quantum computation.

Significance. If the central reduction and encodings are sound, the work supplies the first machine-checked distance certificates for industrially viable qLDPC codes at scales where hand proofs are infeasible and unverified solvers leave a trust gap. Credit is due for the self-contained formalization against Lean's kernel, the automatic generation of checked proofs, the parameter-free character of the verified reduction, and the explicit design for reuse in end-to-end fault-tolerant verification efforts.

major comments (2)
  1. [Abstract (pipeline scaling paragraph)] Abstract, paragraph on pipeline scaling: the claim that the verified reduction to SAT together with the BitVec flattening and error-location encoding 'correctly preserves the original mathematical statement inside Lean' is load-bearing for every generated certificate. The manuscript must supply an explicit theorem (with proof sketch) showing that unsatisfiability of the generated instance is equivalent to the absence of any nontrivial logical operator of weight < d, including that the location encoding enumerates every possible low-weight Pauli vector in the normalizer and that the flattening preserves all commutation and weight constraints.
  2. [Abstract and scaling discussion] Abstract and scaling discussion: the headline scaling result to 144 qubits is performed outside the Lean kernel. This severs the end-to-end verification claim for the largest instances; the manuscript must delineate precisely which components (reduction, encoding, distance certificate) remain kernel-checked versus those that rely on external computation, and must state the resulting trust boundary.
minor comments (2)
  1. [Introduction] The [[n, k, d]] notation for code parameters is used without an explicit definition in the opening paragraphs; a brief reminder of its meaning would aid readers outside quantum coding theory.
  2. [Results tables] Figure captions and table headers should explicitly state whether reported distances are lower bounds obtained from the SAT unsatisfiability certificates or upper bounds from other methods.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive review of our manuscript. The comments highlight important points about the presentation of the soundness argument and the trust boundaries in our scaling results. We address each major comment below and will revise the manuscript accordingly to improve clarity and rigor.

read point-by-point responses

  1. Referee: [Abstract (pipeline scaling paragraph)] Abstract, paragraph on pipeline scaling: the claim that the verified reduction to SAT together with the BitVec flattening and error-location encoding 'correctly preserves the original mathematical statement inside Lean' is load-bearing for every generated certificate. The manuscript must supply an explicit theorem (with proof sketch) showing that unsatisfiability of the generated instance is equivalent to the absence of any nontrivial logical operator of weight < d, including that the location encoding enumerates every possible low-weight Pauli vector in the normalizer and that the flattening preserves all commutation and weight constraints.

    Authors: We agree that the soundness of the reduction is central and that an explicit statement strengthens the manuscript. In the revised version we will insert a new theorem (with accompanying proof sketch) in the main text, stating that unsatisfiability of the generated SAT instance is equivalent to the non-existence of any nontrivial logical operator of weight less than d. The sketch will explain how the error-location encoding enumerates all candidate low-weight Pauli vectors in the normalizer and how the BitVec flattening preserves the original commutation relations and Hamming-weight constraints. The theorem will be accompanied by the corresponding Lean statement. revision: yes

  2. Referee: [Abstract and scaling discussion] Abstract and scaling discussion: the headline scaling result to 144 qubits is performed outside the Lean kernel. This severs the end-to-end verification claim for the largest instances; the manuscript must delineate precisely which components (reduction, encoding, distance certificate) remain kernel-checked versus those that rely on external computation, and must state the resulting trust boundary.

    Authors: We accept the need for a precise delineation. The revised abstract and scaling discussion will explicitly separate the components: the formalization of stabilizer-code theory, the verified reduction to SAT, the BitVec and error-location encodings, and the generation of the Lean-checked proof certificate are all performed inside the kernel. For the 144-qubit instances the SAT-solving step itself is executed externally; the resulting unsatisfiability certificate is then imported and checked inside Lean. We will state the resulting trust boundary: full kernel-checked end-to-end verification holds for the smaller codes (including the [[90,8,10]] and [[70,6,9]] examples), while larger instances rely on the external solver for the final unsatisfiability step, with the reduction and encoding remaining verified. revision: yes

Circularity Check

0 steps flagged

No circularity: verified reduction and encodings are machine-checked against Lean kernel

full rationale

The paper's derivation consists of formalizing stabilizer codes, the binary symplectic representation, and the distance condition inside Lean 4, followed by a verified reduction of the no-low-weight-logical-operator statement to unsatisfiability of a generated SAT instance. The BitVec flattening and the error-location encoding (reducing variables from n to k⌈log₂ n⌉) are themselves part of the Lean formalization whose correctness is checked by the kernel. No equation or claim reduces by construction to a fitted parameter, a self-citation, or an ansatz imported from prior work by the same authors; the central equivalence is established by explicit, machine-verified proofs rather than by renaming or re-using the target result. The library is therefore self-contained against an external, independently implemented proof assistant.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The formalization rests on standard mathematical axioms for linear algebra over GF(2), the Pauli group, and the symplectic representation; no free parameters or invented entities are introduced to obtain the distance certificates.

axioms (2)
  • standard math Linear algebra and group theory over finite fields as formalized in Lean's mathlib
    Invoked throughout the stabilizer code and binary symplectic representation sections.
  • domain assumption Correctness of the verified reduction from distance condition to Boolean satisfiability
    Central to breaking the combinatorial barrier; location: pipeline description in abstract.

pith-pipeline@v0.9.0 · 5854 in / 1431 out tokens · 40805 ms · 2026-05-20T18:41:08.264133+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

32 extracted references · 32 canonical work pages · 1 internal anchor

  1. [1]

    Suppressing quantum errors by scaling a surface code logical qubit.Nature, 614(7949):676–681, 2023

    work page 2023

  2. [2]

    Quantum error correction below the surface code threshold.Nature, 638(8052):920–926, 2025

    work page 2025

  3. [3]

    Aristotle: IMO-level Automated Theorem Proving

    Tudor Achim, Alex Best, Alberto Bietti, Kevin Der, Mathïs Fédérico, Sergei Gukov, Daniel Halpern- Leistner, Kirsten Henningsgard, Yury Kudryashov, Alexander Meiburg, et al. Aristotle: Imo-level automated theorem proving.arXiv preprint arXiv:2510.01346, 2025

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  4. [4]

    Mathematics in lean, 2020

    Jeremy Avigad and Patrick Massot. Mathematics in lean, 2020. 21

    work page 2020

  5. [5]

    Efficient quantum algorithms for simulating sparse hamiltonians.Communications in Mathematical Physics, 270(2):359–371, 2007

    Dominic W Berry, Graeme Ahokas, Richard Cleve, and Barry C Sanders. Efficient quantum algorithms for simulating sparse hamiltonians.Communications in Mathematical Physics, 270(2):359–371, 2007

    work page 2007

  6. [6]

    Cadical 2.0

    Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. Cadical 2.0. InInternational Conference on Computer Aided Verification, pages 133–152. Springer, 2024

    work page 2024

  7. [7]

    Cross, Jay M

    Sergey Bravyi, Andrew W. Cross, Jay M. Gambetta, Dmitri Maslov, Patrick Rall, and Theodore J. Yoder. High-threshold and low-overhead fault-tolerant quantum memory.Nature, 627:778–782, 2024

    work page 2024

  8. [8]

    FLT, 2025

    Kevin Buzzard and Richard Taylor. FLT, 2025

    work page 2025

  9. [9]

    Efficient certified rat verification

    Luís Cruz-Filipe, Marijn JH Heule, Warren A Hunt Jr, Matt Kaufmann, and Peter Schneider-Kamp. Efficient certified rat verification. InInternational Conference on Automated Deduction, pages 220–236. Springer, 2017

    work page 2017

  10. [10]

    The Lean 4 theorem prover and programming language

    Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In CADE-28, volume 12699 ofLNCS, pages 625–635. Springer, 2021

    work page 2021

  11. [11]

    Formal verification of quantum stabiliser codes by stabiliser formalism

    Qiuyi Feng. Formal verification of quantum stabiliser codes by stabiliser formalism

    work page

  12. [12]

    Surviving as a quantum computer in a classical world

    Daniel Gottesman. Surviving as a quantum computer in a classical world. 2024

    work page 2024

  13. [13]

    Quantum algorithm for linear systems of equations

    Aram W Harrow, Avinatan Hassidim, and Seth Lloyd. Quantum algorithm for linear systems of equations. Physical review letters, 103(15):150502, 2009

    work page 2009

  14. [14]

    A verified optimizer for quantum circuits.Proceedings of the ACM on Programming Languages, 5(POPL):1–29, 2021

    Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. A verified optimizer for quantum circuits.Proceedings of the ACM on Programming Languages, 5(POPL):1–29, 2021

    work page 2021

  15. [15]

    Efficient formal verification of quantum error correcting programs.Proceedings of the ACM on Programming Languages, 9(PLDI):1068– 1093, 2025

    Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, and Mingsheng Ying. Efficient formal verification of quantum error correcting programs.Proceedings of the ACM on Programming Languages, 9(PLDI):1068– 1093, 2025

    work page 2025

  16. [16]

    QEClean.https://github.com/Stavan-Jain/QECLean, 2026

    Stavan Jain. QEClean.https://github.com/Stavan-Jain/QECLean, 2026

    work page 2026

  17. [17]

    On the hardness of the minimum distance problem of quantum codes.IEEE Transactions on Information Theory, 69(10):6293–6302, October 2023

    Upendra Kapshikar and Srijita Kundu. On the hardness of the minimum distance problem of quantum codes.IEEE Transactions on Information Theory, 69(10):6293–6302, October 2023

    work page 2023

  18. [18]

    Prime Number Theorem and More, January 2024

    Alex Kontorovich and Terence Tao. Prime Number Theorem and More, January 2024

    work page 2024

  19. [19]

    Formal verification of quantum algorithms using quantum Hoare logic

    Junyi Liu, Bohua Zhan, Shuling Zhu, Shenggang Ying, and Mingsheng Ying. Formal verification of quantum algorithms using quantum Hoare logic. InCAV 2019, volume 11562 ofLNCS, pages 187–207. Springer, 2019

    work page 2019

  20. [20]

    Quantum computational chemistry.Reviews of Modern Physics, 92(1):015003, 2020

    Sam McArdle, Suguru Endo, Alán Aspuru-Guzik, Simon C Benjamin, and Xiao Yuan. Quantum computational chemistry.Reviews of Modern Physics, 92(1):015003, 2020

    work page 2020

  21. [21]

    Quantum information in lean

    Alex Meiburg. Quantum information in lean. https://github.com/Timeroot/Lean-QuantumInfo, 2024

    work page 2024

  22. [22]

    A formalization of the generalized quantum stein’s lemma in lean.arXiv preprint arXiv:2510.08672, 2025

    Alex Meiburg, Leonardo A Lessa, and Rodolfo R Soldati. A formalization of the generalized quantum stein’s lemma in lean.arXiv preprint arXiv:2510.08672, 2025

    work page arXiv 2025

  23. [23]

    A formally certified end-to-end implementation of shor’s factorization algorithm.Proceedings of the National Academy of Sciences, 120(21):e2218775120, 2023

    Yuxiang Peng, Kesha Hietala, Runzhou Tao, Liyi Li, Robert Rand, Michael Hicks, and Xiaodi Wu. A formally certified end-to-end implementation of shor’s factorization algorithm.Proceedings of the National Academy of Sciences, 120(21):e2218775120, 2023

    work page 2023

  24. [24]

    Demonstration of fault-tolerant steane quantum error correction.PRX Quantum, 5(3):030326, 2024

    Lukas Postler, Friederike Butt, Ivan Pogorelov, Christian D Marciniak, Sascha Heußen, Rainer Blatt, Philipp Schindler, Manuel Rispler, Markus Müller, and Thomas Monz. Demonstration of fault-tolerant steane quantum error correction.PRX Quantum, 5(3):030326, 2024

    work page 2024

  25. [25]

    Quantum computing in the nisq era and beyond.Quantum, 2:79, August 2018

    John Preskill. Quantum computing in the nisq era and beyond.Quantum, 2:79, August 2018. 22

    work page 2018

  26. [26]

    Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer.SIAM review, 41(2):303–332, 1999

    Peter W Shor. Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer.SIAM review, 41(2):303–332, 1999

    work page 1999

  27. [27]

    The Lean Mathematical Library

    The mathlib Community. The Lean Mathematical Library. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January

    work page 2020

  28. [28]

    Coble, Thomas Dellaert, Dmitri Maslov, Martin Roetteler, Edwin Tham, Mark Webster, Min Ye, John Gamble, Andrii Maksymov, J

    Felix Tripier, Woo Chang Chung, Jacob Young, Safwan Alam, Bryce Bjork, Aharon Brodutch, Finn Lasse Buessen, Nolan J. Coble, Thomas Dellaert, Dmitri Maslov, Martin Roetteler, Edwin Tham, Mark Webster, Min Ye, John Gamble, Andrii Maksymov, J. P. Marceaux, and Nicolas Delfosse. Fault-tolerant quantum computing with trapped ions: The walking cat architecture, 2026

    work page 2026

  29. [29]

    The intractability of computing the minimum distance of a code.IEEE Transactions on Information Theory, 43(6):1757–1766, 2002

    Alexander Vardy. The intractability of computing the minimum distance of a code.IEEE Transactions on Information Theory, 43(6):1757–1766, 2002

    work page 2002

  30. [30]

    Distance-finding algorithms for quantum codes and circuits, 2026

    Mark Webster, Abraham Jacob, and Oscar Higgott. Distance-finding algorithms for quantum codes and circuits, 2026

    work page 2026

  31. [31]

    Qecv: Quantum error correction verification.arXiv preprint arXiv:2111.13728, 2021

    Anbang Wu, Gushu Li, Hezi Zhang, Gian Giacomo Guerreschi, Yuan Xie, and Yufei Ding. Qecv: Quantum error correction verification.arXiv preprint arXiv:2111.13728, 2021

    work page arXiv 2021

  32. [32]

    Coqq: Foundational verification of quantum programs.Proceedings of the ACM on Programming Languages, 7(POPL):833– 865, 2023

    Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying. Coqq: Foundational verification of quantum programs.Proceedings of the ACM on Programming Languages, 7(POPL):833– 865, 2023. 23

    work page 2023