Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory

Quantum information theory underpins quantum computing and communication, but formalizing its theorems in machine-checkable form has lacked reusable infrastructure. This paper presents a Lean 4 library providing composable, verified building blocks for quantum states, channels, codes, and rate constructions, used to formally prove major theorems like Schumacher's source-coding theorem and the Holevo-Schumacher-Westmoreland capacity theorem. Applications include rigorous, bug-free verification of quantum communication protocols, a foundation for future automated theorem proving in quantum information science, and a knowledge base enabling AI-assisted formalization and agentic reasoning in quantum computing research. Authors: Chengkai Zhu, Ziao Tang, Guocheng Zhen, Yimeng Cao, Yusheng Zhao, Ranyiliu Chen, Xuanqiang Zhao, Lei Zhang, Xin Wang Paper: https://arxiv.org/abs/2607.09632v1