{"id":"arxiv/2607.09632","url":"https://arxiv.org/abs/2607.09632","tags":["quant-ph","cs.AI"],"score":0,"title":"Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory","domain":"quant-ph","source":"arxiv","authors":["Chengkai Zhu","Ziao Tang","Guocheng Zhen","Yimeng Cao","Yusheng Zhao","Ranyiliu Chen","Xuanqiang Zhao","Lei Zhang","Xin Wang"],"reviews":0,"subject":"quant-ph","summary":"Quantum information theory (QIT) characterizes the capabilities and fundamental limits of quantum information processing, underpinning quantum communication, computation, and error correction. Formalizing its coding theorems requires connecting finite-block protocols, analytic inequalities, and asymptotic limits within a unified machine-checked framework. Existing developments, however, lack a reusable operational layer that defines codes, error criteria, achievable rates, and capacities independently of their information-theoretic characterizations. In this work, we present LeanQIT, a Lean…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"discussed":0,"published":"2026-07-10","reactions":{}}