The Generalized Quantum Stein's Lemma is a theorem in quantum hypothesis testing that provides an operational meaning to the relative entropy within the context of quantum resource theories. Its original proof was found to have a gap, which led to a search for a corrected proof. We formalize the proof presented in [Hayashi and Yamasaki (2024)] in the Lean interactive theorem prover. This is the most technically demanding theorem in physics with a computer-verified proof to date, building with a variety of intermediate results from topology, analysis, and operator algebra. In the process, we rectified minor imprecisions in [HY24]'s proof that formalization forces us to confront, and refine a more precise definition of quantum resource theory. Formalizing this theorem has ensured that our Lean-QuantumInfo library, which otherwise has begun to encompass a variety of topics from quantum information, includes a robust foundation suitable for a larger collaborative program of formalizing quantum theory more broadly.

翻译：广义量子Stein引理是量子假设检验中的一个定理，它在量子资源理论的背景下为相对熵提供了操作意义。其原始证明被发现存在缺陷，这促使人们寻找修正后的证明。我们在Lean交互式定理证明器中形式化了[Hayashi和Yamasaki（2024）]中提出的证明。这是迄今为止物理学中技术难度最高、且具有计算机验证证明的定理，其构建过程综合运用了拓扑学、分析学和算子代数中的多种中间结果。在此过程中，我们修正了[HY24]证明中因形式化要求而必须面对的细微不精确之处，并完善了量子资源理论的更精确定义。对该定理的形式化确保了我们开发的Lean-QuantumInfo库——该库已开始涵盖量子信息领域的多种主题——具备了稳健的基础，足以支撑更广泛地形式化量子理论的更大规模合作计划。