Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory
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 4
Lineage graph
Paper → model → repo connections mined from source citations (Tier-1 exact match).
Why these links exist
Every edge carries a method, confidence, and the source snippet that justified it — so bad links are debuggable.
- LinkedLinked via arxiv author · 85%Chengkai Zhu →
“Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory”
- LinkedLinked via arxiv author · 85%Ziao Tang →
“Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory”
- LinkedLinked via arxiv author · 85%Guocheng Zhen →
“Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory”
- LinkedLinked via arxiv author · 85%Yimeng Cao →
“Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory”
- LinkedLinked via arxiv author · 85%Yusheng Zhao →
“Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory”
- LinkedLinked via arxiv author · 85%Ranyiliu Chen →
“Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory”
- LinkedLinked via arxiv author · 85%Xuanqiang Zhao →
“Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory”
- LinkedLinked via arxiv author · 85%Lei Zhang →
“Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory”