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

arXiv: https://arxiv.org/abs/2607.09632 · HTML: https://mlsanity.com/paper/2607.09632/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 45 references that are in the map.
- First posted on arXiv 10 Jul 2026.

## Builds on (most cited first, 7 of 7)

- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [A Formalization of the Generalized Quantum Stein's Lemma in Lean](https://mlsanity.com/paper/2510.08672/) (2025)
- [AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities](https://mlsanity.com/paper/2606.26442/) (2026)
- [End-to-End Formalization of Quantum Error Correction](https://mlsanity.com/paper/2605.16523/) (2026)
- [A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm](https://mlsanity.com/paper/2204.07112/) (2022)
- [A Machine-Verified Proof of a Quantum-Optimization Conjecture](https://mlsanity.com/paper/2606.29687/) (2026)
- [Certified Quantum Computation in Isabelle/HOL](https://mlsanity.com/paper/2012.13925/) (2020)

## Built on by (most cited first, 2 of 2)

- [AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics](https://mlsanity.com/paper/2609.05157/) (2026)
- [A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCs](https://mlsanity.com/paper/2609.10579/) (2026)

## Abstract (arXiv)

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 library for finite-dimensional QIT. It provides composable, kernel-checked interfaces for quantum states and channels, source and channel codes, finite-block performance criteria, hypothesis testing, one-shot quantities, and asymptotic rate constructions. Using this infrastructure, we formalize Schumacher's quantum source-coding theorem, the Holevo--Schumacher--Westmoreland classical-capacity theorem, and the entanglement-assisted classical-capacity theorem together with its strong converse. By separating operational definitions from analytic characterizations and exposing reusable achievability, converse, and asymptotic components, Lean-QIT provides a machine-readable foundation for formal QIT and a compositional knowledge substrate for emerging AI-assisted formalization, automated proof search, and agentic reasoning in quantum information and computation.