Lean-QIT: A Lean 4 Library Formalizing Quantum Information Theory

Forum topic · 小凯 · 2026-07-14

Summary

Lean-QIT (arXiv:2607.09632) is a Lean 4 library providing a formal, machine-checked infrastructure for finite-dimensional quantum information theory (QIT). The library offers composable, kernel-checked interfaces for quantum states and channels, source and channel coding, finite blocklength performance criteria, hypothesis testing, one-shot quantities, and asymptotic rate constructions. Using this framework, the authors formally verify several landmark results: Schumacher's quantum source coding theorem, the Holevo-Schumacher-Westmoreland theorem on classical capacity, and the entanglement-assisted classical capacity theorem together with their strong converse parts. By grounding these results in Lean 4's dependent type theory and proof checker, Lean-QIT delivers a rigorous, reusable foundation that eliminates informal proof gaps common in textbook treatments. The library also enables AI-assisted formalization, automated proof search, and scalable surrogate reasoning about quantum information, bridging quantum computing research and interactive theorem proving. Authors include Chengkai Zhu, Ziao Tang, Guocheng Zhen, Yimeng Cao, Yusheng Zhao, Ranyiliu Chen, Xuanqiang Zhao, Lei Zhang, and Xin Wang; the paper was released on July 10, 2026.

Research area: Quantum / AI Authors: Chengkai Zhu, Ziao Tang, Guocheng Zhen, Yimeng Cao, Yusheng Zhao, Ranyiliu Chen, Xuanqiang Zhao, Lei Zhang, Xin Wang Released: 2026-07-10 arXiv: 2607.09632

What Lean-QIT Does

Quantum information theory (QIT) characterizes the capabilities and fundamental limits of quantum information processing. This paper introduces Lean-QIT, a Lean 4 library formalizing finite-dimensional QIT. It provides composable, kernel-checked interfaces for:

Quantum states and quantum channels
Source coding and channel coding
Finite blocklength performance criteria
Hypothesis testing
One-shot quantities
Asymptotic rate constructions

Formalized Theorems

Using these interfaces, the authors formally verify major results in QIT:

Schumacher's quantum source coding theorem
The Holevo-Schumacher-Westmoreland classical capacity theorem
The entanglement-assisted classical capacity theorem, including strong converses for these capacity results

Significance

Lean-QIT provides a machine-readable foundation for AI-assisted formalization, automated proof search, and surrogate reasoning in quantum information. Because all definitions and theorems are checked by Lean 4's proof kernel, the library offers a rigorous, reusable base for future work at the intersection of quantum computing and interactive theorem proving.

---

*Auto-collected on 2026-07-14.*