{"id":"arxiv/2605.16523","url":"https://arxiv.org/abs/2605.16523","tags":["quant-ph","cs.LO"],"score":0,"title":"End-to-End Formalization of Quantum Error Correction","domain":"quant-ph","source":"arxiv","authors":["Mattias Ehatamm","Yi Lee","Xiaodi Wu","Runzhou Tao"],"reviews":0,"subject":"quant-ph","summary":"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…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"discussed":0,"published":"2026-05-15","reactions":{}}