知识卡片：Lean-QIT：面向量子信息理论的形式化基础设施

一句话结论：Lean-QIT 是一个基于 Lean 4 的开源形式化库，首次将量子信息理论中的三个核心编码定理（Schumacher 量子信源编码、Holevo-Schumacher-Westmoreland 经典容量、纠缠辅助经典容量及其强逆）在机器可检查的框架中统一实现，为量子信息的形式化验证和 AI 辅助推理提供了可复用的操作层。

研究问题：量子信息理论（QIT）的编码定理需要将有限块协议、解析不等式和渐近极限连接到一个统一的机器可检查框架中。现有工作缺乏一个可复用的操作层来独立于信息论特征定义码、错误准则、可达速率和容量。本文旨在填补这一空白。

方法/产品要点：

• Lean 4 库：Lean-QIT 是一个针对有限维 QIT 的正式化库，提供可组合、内核检查的接口。
• 核心模块：包括量子态与信道、信源与信道编码、有限块性能准则、假设检验、单次量、渐近速率构造。
• 分离原则：将操作定义（码、错误准则等）与解析特征（熵、互信息等）明确分离，暴露可复用的可达性、逆命题和渐近分量。
• 形式化定理：
  • Schumacher 量子信源编码定理
  • Holevo-Schumacher-Westmoreland 经典容量定理
  • 纠缠辅助经典容量定理及其强逆

主要结果或产业意义：首次在 Lean 4 中形式化了多个 QIT 核心编码定理，提供了一个机器可读的基础设施。这为未来 AI 辅助形式化、自动化证明搜索以及量子信息与计算中的智能体推理提供了组合式知识基底。

为什么重要：

• 填补了形式化 QIT 中可复用的操作层缺失。
• 展示了如何将复杂的渐近编码定理分解为模块化、可验证的组件。
• 为量子密码学、量子通信协议的形式化验证铺平道路；可与 AI 系统结合加速定理证明。
• （与已有卡片无直接重复；本卡片聚焦形式化验证基础设施，而非环境或市场模拟。）

局限与不确定性：

• 当前仅处理有限维量子系统（无限维情况待扩展）。
• 形式化范围限于三个编码定理；更多定理（如信道编码逆界的精确形式、量子网络编码等）尚未覆盖。
• 库的易用性与社区采纳度待实际验证。

可用于图书/PPT/简报的角度：

• 展示形式化方法如何用于验证前沿物理理论（量子信息）
• 作为案例说明“操作层与解析层分离”的设计思想在形式化验证中的优势
• 引用为“AI + 形式化”交叉方向的具体成果
• 可用于量子计算教育中关于编码定理严格证明的补充材料

英文标题：Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory

英文关键词：Quantum information theory; formal verification; Lean 4; coding theorems; machine-checked proofs

原始材料：arXiv:2607.09632v1 (quant-ph, cs.AI) | URL: https://arxiv.org/abs/2607.09632v1