Lean-QIT：迈向量子信息理论的形式化基础设施
Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory
浏览论文内容
中文总结 AI 辅助
研究旨在为量子信息理论构建形式化基础设施，通过Lean 4库LeanQIT提供相关接口，将多个重要定理形式化，分离操作定义与解析表征，为形式化QIT及相关推理提供基础和知识底物。
中文摘要 AI 辅助
量子信息理论（QIT）刻画了量子信息处理的能力和基本极限，支撑着量子通信、计算和纠错。将其编码定理形式化需要在统一的机器检查框架内连接有限块协议、解析不等式和渐近极限。然而，现有进展缺乏一个可重复使用的操作层来独立于信息理论表征定义代码、错误标准、可实现速率和容量。在这项工作中，我们展示了LeanQIT，一个用于有限维QIT的Lean 4库。它为量子态和信道、源和信道编码、有限块性能标准、假设检验、单次量和渐近速率构造提供了可组合、内核检查的接口。利用这个基础设施，我们将舒马赫的量子源编码定理、霍列沃-舒马赫-韦斯特摩兰经典容量定理以及纠缠辅助经典容量定理及其强逆定理形式化。通过将操作定义与解析表征分离，并展示可重复使用的可达性、逆定理和渐近组件，Lean-QIT为形式化QIT提供了机器可读的基础，为量子信息和计算中新兴的人工智能辅助形式化、自动证明搜索和智能推理提供了组合知识基础。
英文摘要
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.
发表机构
- QudeLeap Research（QudeLeap研究院）
- The Hong Kong University of Science and Technology (Guangzhou)（香港科技大学（广州））
- Quantum Science Center of Guangdong-Hong Kong-Macao Greater Bay Area（粤港澳大湾区量子科学中心）
- The University of Hong Kong（香港大学）
机构由 AI 辅助整理，请以论文原文为准。
