在Lean中的广义量子斯坦不等式正式化
量子物理
2025-10-13 v1 计算机科学中的逻辑
摘要
广义量子斯坦不等式是量子假设检验中的一个定理，为量子资源论中的相对熵提供了操作意义。其原始证明被发现存在漏洞，随后寻找了纠正后的证明。我们在Lean交互式定理证明器中形式化了Hayashi和Yamasaki（2024）[HY24]提出的证明。这迄今为止技术上最具挑战性的物理定理计算机验证证明，构建于拓扑学、分析和算子代数等多种中间结果之上。在此过程中，我们纠正了[HY24]证明中的若干细微不严谨之处，形式化过程迫使我们直面并细化量子资源论的更精确定义。对该定理的形式化确保了我们Lean-QuantumInfo库——该库原本涵盖了来自量子信息的各种主题——具备适合更大规模量子理论形式化协作计划的坚实基础。
引用
@article{arxiv.2510.08672,
title = {A Formalization of the Generalized Quantum Stein's Lemma in Lean},
author = {Alex Meiburg and Leonardo A. Lessa and Rodolfo R. Soldati},
journal= {arXiv preprint arXiv:2510.08672},
year = {2025}
}
备注
20 pages, 2 figures, 7 code listings