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.

翻译：量子纠错码（QECC）位于有噪量子硬件与可靠计算之间，因此实际使用的码参数必须可信。衡量一个码性能的单一指标是距离，但验证距离下界在一般情况下是NP难问题，这使得手工证明和直接编写证明辅助脚本都难以实现。因此，文献中的距离值或来自非扩展性的手工证明，或来自未经验证的求解器——在码本应提供保证之处，恰恰留下了信任缺口。我们提出Lean-QEC，这是首个利用Lean 4对稳定子码理论进行形式化验证的工作，能够以工业级码规模实现端到端、机器校验的距离认证。Lean-QEC形式化了量子比特态的线性代数、泡利群、稳定子码、二进制辛表示、经典编码理论，以及CSS码和双变量自行车码族。为突破组合爆炸瓶颈，Lean-QEC通过一个经验证的归约将距离条件转化为布尔可满足性公式。该流水线通过两个编码实现扩展：一是使用BitVec平面化编码替代Lean的矩阵表示，二是采用错误位置编码将变量数从$n$减少至$k\lceil \log_2 n\rceil$。借助这些方法，我们为双变量自行车码和广义自行车码族中一系列工业可行的量子低密度奇偶校验码自动生成了经Lean校验的距离证明，包括[[90, 8, 10]]和[[70, 6, 9]]双变量自行车码，且该形式化方法在Lean内核外可扩展至144量子比特。所生成的库具有可复用性，并设计为可融入更广泛的基于Lean的容错量子计算端到端验证工作。