Delphi.science

QECert: Formal Foundations for Quantum Error-Correction Theory in Lean

Source: arxiv.org/abs/2611.05047

Keming He, Jiahan Chen, Enji Xiong, Zhongyi Ni, Lei Zhang, Xin Wang

arXivarxiv/2611.05047Nov 3, 2026quant-phscore 0

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…

JSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/arxiv/2611.05047
curl -X POST /api/v1/records/arxiv/2611.05047/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2611.05047/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'