量子科技中心_量科网

“广义量子斯坦引理”是量子假设检验中的一个定理，它为量子资源理论框架下的相对熵赋予了操作意义。该定理原始证明中被发现的漏洞促使学界寻求修正方案。该研究团队基于[林和山崎（2024）]提出的证明方案，在Lean交互式定理证明器中完成了形式化验证——这是迄今物理学领域技术复杂度最高且获得计算机验证的定理，其构建过程整合了拓扑学、分析学和算子代数等多个领域的中间结果。在形式化过程中，团队修正了[HY24]证明中因形式化要求而暴露的若干细微不严谨之处，并提炼出更精确的量子资源理论定义。该定理的形式化验证确保了Lean-QuantumInfo程序库（一个已开始涵盖量子信息多领域议题的工具库）具备足够坚实的理论基础，为后续更大规模的量子理论协作形式化项目奠定了基础。