量子信息理论（QIT）描述了量子信息处理的能力和基本限制，支撑着量子通信、计算和纠错。为了形式化其编码定理，需要在一个统一的机器检查框架内连接有限块协议、解析不等式和渐近极限。然而，现有的发展缺乏一个可重用的操作层，独立于信息理论表征来定义编码、错误标准、可实现的速率和容量。
在这项工作中，我们提出了 Lean-QIT，这是一个用于有限维量子信息理论的 Lean 4 库。它提供了可组合的、内核检查的接口，用于量子态和通道、源和通道编码、有限块性能标准、假设检验、单次量和渐近速率构造。利用这一基础设施，我们形式化了 Schumacher 的量子源编码定理、Holevo--Schumacher--Westmoreland 经典容量定理以及伴随其强对偶的纠缠辅助经典容量定理。
通过将操作定义与解析表征分离，并暴露可重用的可实现性、对偶性和渐近组件，Lean-QIT 为正式的量子信息理论提供了一个机器可读的基础，并为新兴的 AI 辅助形式化、自动化证明搜索和量子信息与计算中的智能推理提供了一个组成知识基础。
博主点评： Lean-QIT 的提出为量子信息理论的形式化提供了强有力的支持，尤其是在定义和验证量子编码定理方面的创新。其可重用的操作层设计不仅提高了效率，也为未来的量子计算研究奠定了坚实的基础。该工具的开发将极大推动量子信息科学的进步。