By creating reusable, composable building blocks for quantum information theory in a formal proof system, this work enables both human verification and AI-assisted discovery of quantum communication and computation limits.
Lean-QIT is a formal library in Lean 4 that provides machine-checked definitions and proofs for quantum information theory. It separates operational concepts (codes, channels, error criteria) from their mathematical characterizations, enabling rigorous formalization of key theorems like Schumacher's source-coding theorem and the Holevo-Schumacher-Westmoreland capacity theorem.