Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory
Published in arXiv preprint, 2026
LeanQIT is a Lean 4 library that supplies a reusable, machine-checked operational foundation for finite-dimensional quantum information theory. It covers states and channels, coding protocols, error criteria, hypothesis testing, one-shot quantities, and asymptotic rates. The library is used to formalize Schumacher source coding, Holevo–Schumacher–Westmoreland classical capacity, and entanglement-assisted classical capacity together with its strong converse. Its modular design also provides structured knowledge for automated proof search and AI-assisted formalization.