The authors present LeanQIT, a Lean 4 library designed to provide a reusable operational layer for finite-dimensional quantum information theory (QIT). This infrastructure defines codes, error criteria, achievable rates, and capacities independently of their information-theoretic characterizations.
- Provides composable, kernel-checked interfaces for quantum states, channels, source and channel codes, and hypothesis testing.
- Formalizes Schumacher's quantum source-coding theorem, the Holevo--Schumacher--Westmoreland classical-capacity theorem, and the entanglement-assisted classical-capacity theorem with its strong converse.
- Exposes reusable achievability, converse, and asymptotic components to separate operational definitions from analytic characterizations.
Lean-QIT offers a machine-readable foundation for formal QIT and serves as a compositional knowledge substrate for AI-assisted formalization, automated proof search, and agentic reasoning.