{"id":"arxiv/2611.05047","url":"https://arxiv.org/abs/2611.05047","tags":["quant-ph"],"score":0,"title":"QECert: Formal Foundations for Quantum Error-Correction Theory in Lean","domain":"quant-ph","source":"arxiv","authors":["Keming He","Jiahan Chen","Enji Xiong","Zhongyi Ni","Lei Zhang","Xin Wang"],"reviews":0,"subject":"quant-ph","summary":"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…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"discussed":0,"published":"2026-11-03","reactions":{}}