Lean-QIT：迈向量子信息论的形式化基础设施

量子信息论（QIT）刻画了量子信息处理的能力与基本极限，支撑着量子通信、量子计算和量子纠错。将其编码定理形式化，需要在统一的机器验证框架内连接有限块协议、解析不等式和渐近极限。然而，现有进展缺乏一个可复用的操作层，该层独立于其信息论刻画来定义码、误差准则、可达速率和容量。在本工作中，我们提出 LeanQIT，一个用于有限维 QIT 的 Lean 4 库。它为量子态与量子信道、信源与信道码、有限块性能准则、假设检验、单发数量与渐近速率构造提供了可组合的、内核验证的接口。利用该基础设施，我们形式化了 Schumacher 量子信源编码定理、Holevo–Schumacher–Westmoreland 经典容量定理，以及纠缠辅助经典容量定理及其强逆定理。通过将操作定义与解析刻画分离，并暴露可复用的可达性、逆定理与渐近组件，Lean-QIT 为形式化 QIT 提供了机器可读的基础，并为新兴的 AI 辅助形式化、自动化证明搜索以及量子信息与计算中的智能体推理提供了组合式知识基底。