Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory
📄 arXiv:2607.09632 · 📥 PDF · 2026-07-10 · quant-ph
Authors: Chengkai Zhu [arXiv · scholar] , Ziao Tang [arXiv · scholar] , Guocheng Zhen [arXiv · scholar] , Yimeng Cao [arXiv · scholar] , Yusheng Zhao [arXiv · scholar] , Ranyiliu Chen [arXiv · scholar] , Xuanqiang Zhao [arXiv · scholar] , Lei Zhang [arXiv · scholar] , Xin Wang [arXiv · scholar]
🕰 Orloj analysis
Tento článek představuje LeanQIT, knihovnu v Lean 4 pro formalizaci kvantové informační teorie (QIT), která poskytuje strojově ověřená rozhraní pro základní koncepty QIT. Pomocí této infrastruktury formalizuje klíčové teorémy jako Schumacherův teorém a Holevo-Schumacher-Westmorelandův teorém.
💡 Práce nabízí cennou formální infrastrukturu pro QIT, což je spíše inženýrský než teoretický průlom, ale s vysokou hodnotou pro rigorózní ověřování a budoucí AI-asistovanou formalizaci.
Categories:
INF-3
INF-1
MET-1
INF-2
✓ code_available, falsifiable, modest_claims
📄 Abstract
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.