作者提出了 LeanQIT，这是一个旨在为有限维量子信息论（QIT）提供可重用操作层的 Lean 4 库。该基础设施独立于其信息论特征来定义编码、错误标准、可达速率和容量。

  • 为量子态、信道、源和信道编码以及假设检验提供可组合的内核检查接口。
  • 形式化了 Schumacher 的量子信源编码定理、Holevo--Schumacher--Westmoreland 经典容量定理以及具有强逆命题的纠缠辅助经典容量定理。
  • 暴露可重用的可达性、逆命题和渐近组件，以将操作定义与分析特征分离。

Lean-QIT 为形式化 QIT 提供了机器可读的基础，并作为 AI 辅助形式化、自动证明搜索和代理推理的可组合知识基底。