QECert: Formal Foundations for Quantum Error-Correction Theory in Lean
Abstract
Quantum error correction provides the mathematical basis for protecting quantum information against noise. Existing formalizations have established foundations for stabilizer codes and code verification. However, a systematic formal treatment of the asymptotic constructions and fundamental limitations that underpin scalable quantum error correction is still needed. We present QECert, a Lean library providing reusable formal foundations for these theoretical questions. It connects quantum error-correction criteria, stabilizer and Calderbank-Shor-Steane codes, and algebraic and homological constructions within a common framework. Asymptotically good quantum low density parity check codes provide the principal case study. We formalize constructions and asymptotic parameter theorems spanning hypergraph products, balanced products, lifted products, and quantum Tanner codes. Further developments cover Bravyi-Poulin-Terhal bounds and related locality restrictions, constant overhead magic state distillation, and energy barriers and storage errors for quantum memories. QECert establishes a reusable formal foundation for studying the capabilities, resource requirements, and fundamental limitations of quantum error correction, supporting systematic verification and further development of its theory.
Related
- Foundations of Many-Body Theory of Quantum Unified Statistics: Green functions and Linear Response Theory
- Theory of approximate quantum error correction and the error-set model
- Generalizable Equivariant Diffusion Models for Non-Abelian Lattice Gauge Theory: Analytical Foundations and Numerical Scaling Tests
- Statistical foundations of revised reverberation theory for a diffuse sound field in a room
- Attractor-Vascular Coupling Theory: Formal Grounding and Empirical Validation for AAMI-Standard Cuffless Blood Pressure Estimation from Smartphone Photoplethysmography
BibTeX
@misc{he2026qecert,
title = {{QECert: Formal Foundations for Quantum Error-Correction Theory in Lean}},
author = {Keming He and Jiahan Chen and Enji Xiong and Zhongyi Ni and Lei Zhang and Xin Wang},
howpublished = {arXiv},
year = {2026},
month = nov,
doi = {10.48550/arxiv.2611.05047},
eprint = {2611.05047},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2611.05047},
}
RIS
TY - UNPB
TI - QECert: Formal Foundations for Quantum Error-Correction Theory in Lean
AU - Keming He
AU - Jiahan Chen
AU - Enji Xiong
AU - Zhongyi Ni
AU - Lei Zhang
AU - Xin Wang
PY - 2026
DA - 2026/11/03
PB - arXiv
DO - 10.48550/arxiv.2611.05047
UR - https://arxiv.org/abs/2611.05047
AB - Quantum error correction provides the mathematical basis for protecting quantum information against noise. Existing formalizations have established foundations for stabilizer codes and code verification. However, a systematic formal treatment of the asymptotic constructions and fundamental limitations that underpin scalable quantum error correction is still needed. We present QECert, a Lean library providing reusable formal foundations for these theoretical questions. It connects quantum error-correction criteria, stabilizer and Calderbank-Shor-Steane codes, and algebraic and homological constructions within a common framework. Asymptotically good quantum low density parity check codes provide the principal case study. We formalize constructions and asymptotic parameter theorems spanning hypergraph products, balanced products, lifted products, and quantum Tanner codes. Further developments cover Bravyi-Poulin-Terhal bounds and related locality restrictions, constant overhead magic state distillation, and energy barriers and storage errors for quantum memories. QECert establishes a reusable formal foundation for studying the capabilities, resource requirements, and fundamental limitations of quantum error correction, supporting systematic verification and further development of its theory.
ER -