想用机器验证量子编码定理？Lean-QIT在Lean 4里搭好了整套框架，连HSW定理都形式化了，做量子信息形式化研究的朋友可以复用。
哈佛大学研究团队发布了Lean-QIT，一个基于Lean 4定理证明器的库，用于有限维量子信息论的形式化。它提供了量子态、信道、源编码和信道编码的可组合接口，并形式化了Schumacher量子源编码定理、Holevo-Schumacher-Westmoreland经典容量定理及纠缠辅助经典容量定理（含强逆）。该基础设施分离了操作定义与解析刻画，为AI辅助形式化和自动化证明搜索提供了可复用基础。
Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory
Quantum information theory (QIT) characterizes the capabilities and fundamental limits of quantum information processing, underpinning quantum communication, computation, and error correction. Formalizing its coding theorems requires connecting finite-block protocols, analytic inequalities, and asymptotic limits within a unified machine-checked framework. Existing developments, however, lack a reusable operational layer that defines codes, error criteria, achievable rates, and capacities independently of their information-theoretic characterizations. In this work, we present LeanQIT, a Lean 4 library for finite-dimensional QIT. It provides composable, kernel-checked interfaces for quantum states and channels, source and channel codes, finite-block performance criteria, hypothesis testing, one-shot quantities, and asymptotic rate constructions. Using this infrastructure, we formalize Schumacher's quantum source-coding theorem, the Holevo--Schumacher--Westmoreland classical-capacity theorem, and the entanglement-assisted classical-capacity theorem together with its strong converse. By separating operational definitions from analytic characterizations and exposing reusable achievability, converse, and asymptotic components, Lean-QIT provides a machine-readable foundation for formal QIT and a compositional knowledge substrate for emerging AI-assisted formalization, automated proof search, and agentic reasoning in quantum information and computation.