10:46
官方账号arXiv cs.AI@Chengkai Zhu, Ziao Tang, Guocheng Zhen, Yimeng Cao, Yusheng Zhao, Ranyiliu Chen, Xuanqiang Zhao, Lei Zhang, Xin Wang
推荐理由：想用机器验证量子编码定理？Lean-QIT在Lean 4里搭好了整套框架，连HSW定理都形式化了，做量子信息形式化研究的朋友可以复用。
Lean-QIT
共 1 条相关 AI 资讯
7月13日
10:46
哈佛大学研究团队发布了Lean-QIT，一个基于Lean 4定理证明器的库，用于有限维量子信息论的形式化。它提供了量子态、信道、源编码和信道编码的可组合接口，并形式化了Schumacher量子源编码定理、Holevo-Schumacher-Westmoreland经典容量定理及纠缠辅助经典容量定理（含强逆）。该基础设施分离了操作定义与解析刻画，为AI辅助形式化和自动化证明搜索提供了可复用基础。