Quantum error correction provides the mathematical basis for protecting quantum information against noise, and existing formalizations have established foundations for stabilizer codes and code verification. QECert, a Lean library, connects quantum error-correction criteria, stabilizer and Calderbank–Shor–Steane codes, and constructions within a common framework.
Lean library links quantum codes to their error-correction criteria
Quantum error correction provides the mathematical basis for protecting quantum information against noise, and existing formalizations have established foundations for stabilizer codes and code verification. QECert, a Lean library, connects quantum error-correction criteria, stabilizer and Calderbank–Shor–Steane codes, and constructions within a common framework.