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.
- PossiblePossibly related (embedding) · 52%76 Quantum Theorems Completed By AI In New Lean 4 Benchmarks - Quantum Zeitgeist →
- PossiblePossibly related (embedding) · 46%BlueQubit Secures $1.5M DOE Grants For AI-Driven Quantum Error Correction - Quantum Zeitgeist →
- FuzzyOverlapping authors or contributors · 62%bytedance/deer-flow →
“Shared author/contributor keys: wang”
- FuzzyOverlapping authors or contributors · 62%ray-project/ray →
“Shared author/contributor keys: wang”
- 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”