最复杂、最难的机器验证的物理学定理

Lean 中广义量子 Stein 引理的形式化

A Formalization of the Generalized Quantum Stein's Lemma in Lean

https://arxiv.org/abs/2510.08672

广义量子斯坦因引理是量子假设检验中的一个定理，它在量子资源理论的背景下为相对熵提供了操作性意义。其原始证明被发现存在漏洞，这导致了对修正证明的寻找。我们在Lean交互式定理证明器中形式化了[Hayashi和Yamasaki（2024）]中提出的证明。这是迄今为止经过计算机验证证明的物理学中最技术要求高的定理，它结合了来自拓扑学、分析学和算子代数的各种中间结果。在这一过程中，我们纠正了形式化迫使我们面对的[H Y24]证明中的微小不精确之处，并提炼出了量子资源理论的更精确定义。形式化这个定理确保了我们的Lean-QuantumInfo库，该库已经开始涵盖量子信息的多种主题，拥有一个坚实的基础，适合于更广泛地形式化量子理论的更大合作项目。

引言

实验者如何在实验室中验证他们能够访问的量子态？假设检验是统计学中研究这一问题的任务。在量子信息理论中，这项任务与零假设相对比，假设一个状态 ρ，而备择假设则假设一个状态 σ。

除了广义量子斯坦因引理（GQSL）对假设检验和资源理论的重要性外，它还承载着一个有趣的故事：2023年，文献[5]发现文献[3]的原始证明中存在一个漏洞，这随后激发了证明GQSL的努力，最终在文献[6, 7]中完成。这些事件激励我们使用LEAN将引理作为基于证明的量子信息研究的典范目标。

我们在LEAN定理证明器[8-10]中形式化了基于文献[6]的这个广义量子斯坦因引理（GQSL）。为了实现这一目标，必须构建量子信息的底层正式结构，这反过来又需要更基本和基础的数学结构。这一系列依赖关系展示了在LEAN（或其他定理证明语言）中进行证明工作的独特环境。

我们使用广泛使用的MATHLIB[11, 12]库来覆盖所需的基本和基础数学，并且与GQSL一起，我们构建了LEAN-QuantumInfo库[13]来支持其证明。截至2025年10月，该库拥有超过1000个定理、250个定义和15000行代码。

我们相信在LEAN中广泛形式化量子信息的长期目标，就像数学的其他分支在MATHLIB中被形式化一样。同样，我们相信量子信息理论的基于证明的性质使其特别适合于形式化，与其他物理学的子领域相比。

本文的其余部分组织如下。我们在第二节提供证明形式化的背景和GQSL。我们通过讨论无克隆定理的正式化证明来说明前者，该证明在第二节A.1中。我们在第三节中展示了我们形式化的结果，其中我们在LEAN中形式化了主要定理，并评论了它如何被解释并适应MATHLIB和原始证明的更大背景。我们还提到了哪些方面的正式化仍然存在。第四节详细讨论了所考虑的量子资源理论的细节、为了促进、改进或使工作成为可能而必须做出的技术选择，以及形式化过程中使显而易见的复杂性，这些复杂性可能会被忽视。

II. 背景

A. 证明形式化

交互式定理证明，也称为自动定理证明，是使用计算机来构建或检查数学陈述的形式证明[14]。人机交互通过提供证明步骤的编码指令，同时接收反馈，例如证明的正确性和当前状态（见图1）。与符号计算或数值模拟不同，证明验证系统在一个形式逻辑框架内运行：每个定理都是从公理和推理规则中推导出来的，确保正确性由构造保证。

LEAN是领先的交互式定理证明器之一。它基于构造演算，这是一种强大的类型理论基础，统一了编程和逻辑。在LEAN中，数学对象、命题和证明都在同一个类型语言中表示，这种观点通常总结为“命题即类型”。

存在几种其他交互式定理证明器，如Rocc（前Coq）、Isabelle/HOL和Agda，每种都有不同的逻辑基础和证明风格。我们选择LEAN部分是因为MATHLIB，一个广泛的社区驱动的正式化数学库。MATHLIB涵盖了广泛的领域，其中线性代数、分析和拓扑对本项目最有用。此外，LEAN提供了一个证明策略工具箱，可以自动化许多证明步骤，只留下更非平凡的步骤供用户编写。例如，可以通过调用Nat.succ_eq_add_one定理来证明1 + 1 = 2，用1的后继者替换1+1——根据定义等于2——或者简单地应用反射策略rf1。

我们强调LEAN与现代大型语言模型完全不同，后者可以产生合理但不可靠的论点。相反，LEAN接受的每个证明都由一个可信的内核验证到数学的最基本公理。事实上，已经使用LEAN和MATHLIB完成了几个数学形式化项目[15]，还有许多正在进行中。

通过一个简单但足够非平凡的证明步骤来说明是很有启发性的。这样一个陈述，对量子信息科学有广泛而重要的影响，是无克隆定理[16]。在其最简单的形式中，无克隆定理的证明是直接的，并且源于量子理论的基本事实。为了说明LEAN中形式化的工作流程，我们首先用自然语言重现教科书中的证明，然后将其与LEAN中的相应推导进行比较。在附录A中，我们提供了更多在LEAN-QuantumInfo库中证明的与量子信息理论相关的定理示例。

1. 示例：无克隆定理

B. 广义量子斯坦因引理

III. 形式化的结果

我们最终的目标是正式验证文献[6]前半部分中提出的所有陈述，这些陈述导致了广义量子斯坦因引理（GQSL）。特别是，我们目前没有尝试形式化文献的后半部分，该部分将GQSL应用于量子资源理论（QRTs）的第二定律——定理2，“QRTs的状态第二定律。”目前，论文中所有主要定义、引理和定理的陈述几乎与文献[6]中的对应部分一一对应地形式化。从这个意义上说，论文的论点已经被正式验证。

我们还建立了一个广泛的基础量子理论体系，以便大多数定理都有端到端的证明。剩余的陈述可以通过LEAN的 sorry 或 axiom 命令来追踪，我们已经将其简化为一个非常标准的量子理论事实的简短列表。我们剩余的目标是证明这些事实，以便GQSL有一个端到端的证明，我们预计在未来几个月内完成这个项目。我们需要的标准事实包括：

LEAN通过关键字 sorry 促进了未改进定理到开发工作流程的整合：带有标记为 sorry 的证明的定理被LEAN编译器假定为真。因此，人们可以最初专注于陈述结果，推迟证明。

为了说明主要结果（定理1）是如何形式化的，我们解释了它在代码库中的编写方式：

A. 现有证明中的不精确之处

类型理论所要求的一些技术细节在书面数学中根本没有自然的等价物。例如，我们需要证明两个状态之间的相对熵等于在不同但等价的希尔伯特空间下解释的相同状态对之间的相对熵。这些定理——以及它们需要被证明的事实——在我们看来，只是将量子物理嵌入到类型理论语言中的副产品。它们并没有实质上的物理意义。

相反，在任何自然语言证明中，有些步骤可以提供或多或少的细节。在形式化过程中，我们发现文献[6]中的一些地方没有完全解决细节问题。

IV. 设计与开发选择

在形式化过程中，需要做出几个设计选择：数学约定的选择、关于攻击的数学或物理范围的有意义问题，以及一些关于良好软件工程的困难但平凡的选择。

A. 量子理论的基础

“量子理论”有几种不同的基础。最常见的当然是有界算子（等价地，希尔伯特空间上的连续线性映射），其中状态是具有单位迹的正算子。在有限维度的背景下，“有界”或“连续”前缀经常被省略。一个带有基的希尔伯特空间可以被采用为额外的数据，在这种情况下有一个“标准基”可以参考。或者可以忘记希尔伯特空间本身，只留下一个C*-代数[29]。通过采用一个包络W*-代数，可以转而使用冯诺依曼代数[30, 31]作为量子力学的基础。量子场论的公理化，如AQFT[32]，进一步携带了与每个局部代数相关的时空区域的额外数据。还有其他基础存在，如广义概率理论[33-35]。

在LEAN-QUANTUMINFO库开始时，中期目标是从量子计算中形式化语义。在量子比特和电路的背景下，所有计算都在有限维度中完成，并且几乎总是有一个标准基可以作为数据访问。基本上，每个定义，如Pauli门、稳定器状态或电路的输出分布，都需要参考一个基。这激发了选择矩阵作为量子混合态或可观测量的基本概念。此外，我们决定将Hermitian矩阵视为它们自己的一等类型。这意味着什么？物理符号通常在很大程度上建立在围绕不正确组合数据的讨论上，编程语言理论称之为类型安全。例如，很明显表达式

是类型错误的，即使kets和bras在外观上都是“只是”向量，并且可以相减。LEAN中也支持这种功能，我们的Bra和Ket类型都是可推导的向量，但定义上等于向量。同样，如果 H 是一个哈密顿量，U 是一个两量子比特的酉变换，那么表达式

应该是令人担忧的，即使这些都是“只是”矩阵。LEAN的MATHLIB已经定义了一种特殊类型Matrix.unitaryGroup，用于酉变换的类型安全操作（例如，允许乘法，但不允许加法，除非它们被明确剥离为裸矩阵）。我们的库以类似的方式定义了一个HermitianMat类型，用于Hermitian矩阵的类型安全操作，基于现有的MATHLIB谓词Matrix.IsHermitian。这种类型允许实数的加法和乘法，但不允许矩阵乘法；代替乘法，提供了一个类型安全的conj函数，用于

。API的其他好处是矩阵的迹被给定为一个明显实数，而不是一个可以随后证明为实数的复数。

在构建了Loewner序之后，这导致我们定义了混合态，可能是库中最核心的类型：

可以这样理解。MState 是一种数据结构，它引用了另一个数据类型 d；这个其他类型 d 必须是有限且具有合理相等性概念的。（例如，对于一个量子比特，这个其他类型可以是布尔值，或者是字符串对“上”和“下”；对于一对量子比特，它可以是从1或4的数字，或者是布尔值的有序对。）MState 有一个 Hermitian 矩阵 M，其行和列由 d 索引，并且具有复数项。要求是 M 必须是半正定的且具有单位迹。

为什么使用矩阵而不是其他任何一种形式？原因很简单，因为尽可能携带任何可访问的数据是有用的。通过携带一个由 d 标记的标准基，我们给自己提供了访问最大上下文信息的机会，这样（例如）一个状态的魔力总是可以作为一个定义来访问。在此过程中，我们确实失去了对无限维量子理论的访问，但这为我们在处理正确的拓扑细微差别，或确保诸如迹等量在每次操作后总是正确收敛时节省了许多额外的麻烦。最终形式化无限维理论将是必要的，但最好在掌握了有限维形式化的经验后进行。

B. 量子资源理论的定义

广义量子斯坦因引理首先是一个关于量子资源理论的陈述。有几项工作已经给出了量子资源理论的公理化描述[4, 36, 37]，但这些描述在意义上有所不同，并且它们都不够精确，无法直接对应到LEAN的描述。首先，资源理论是描述一组自由态、一组自由操作，还是两者都有（带有一些兼容性条件）？由于我们专注于斯坦因引理的版本，就涉及到正则化熵，我们唯一需要的实际数据是与每个希尔伯特空间相关的自由态集合。我们称之为 FreeStateTheory，这是一个结构，我们在 ResourceTheory 中扩展它以包含自由操作的概念。

资源理论还需要希尔伯特空间上的一个乘积。这通常被描述为张量积，但这并不能唯一确定。考虑一个资源理论，其中爱丽丝和鲍勃拥有不同的状态，以LOCC操作为自由操作。那么爱丽丝拥有2个量子比特而鲍勃拥有0个量子比特是资源理论中的一个希尔伯特空间，并且它与他们各自拥有1个量子比特的希尔伯特空间是同构的。但是当我们取两个各拥有1个量子比特的状态的乘积时，我们需要知道我们映射到哪个希尔伯特空间。因此，希尔伯特空间由其他类型索引，乘积结构是一个映射，我们要求它与张量积非规范同构。这个乘积通常不能是结合的，所以我们还需要一个结合器。

如果我们允许一个维度为1的希尔伯特空间，那么我们实际上重建了一个单子范畴。我们称具有这样空间的资源理论为单位的。当我们说资源理论成为一个（对称）单子范畴时，请注意，这与[37]中的意义不同，[37]也将资源理论描述为一个单子范畴，但他们的范畴中对象是量子态而不是希尔伯特空间。这给出了资源理论的操作中心视角，而我们的 FreeStateTheory（足以证明）只提到了允许的状态。

原则上，[6]中的证明的每个方面似乎即使在非单位范畴中也能通过，我们最初的努力试图捕捉这一点。然而，证明开发过程受到技术困难的困扰，因此我们转而使用单位（单子）资源理论来完成剩余的证明。当证明完成后，将其扩展到非单位资源理论是未来工作的目标。

C. 数值约定

另一个核心决策是是否使用扩展实数。我们确实使用了扩展实数，而不是仅仅使用实数，我们认为这以增加一些论证的复杂性为代价，提高了证明的完整性。这一选择的影响需要理解“无用值”的概念，这需要一些解释。

1. 无用值

在LEAN中，当输出在其他情况下是未定义的时候，采用所谓的“无用值”是一种常见的惯例。例如，一个无限积分“计算”为零，一个不可微函数的导数，或一个无界序列的上极限也是如此。除以零也总是产生零。这可能看起来令人担忧，因为这可能导致定理的含义与其表面意思不符；但这种威胁并不像看起来那么大，因为它只影响定理陈述中使用的定义。例如，核心LEAN中表达自然数 n 满足

的定理表述为：

该定理的陈述仅需要加法、自然数幂和不等式的概念。因此，它对无用值的存在不敏感——尽管涉及除法、积分等的定理当然是证明的一部分。

在LEAN的早期版本中，避免了无用值，除法函数需要证明分母非零。这将导致一个函数签名，如

。这保证了除法在任何地方使用时都表现良好，但会导致其他涉及依赖重写的相关问题。出于这个原因，现在通常更倾向于使用无用值。

1. 扩展非负实数的行为

量子相对熵的教科书定义[39]如下所述：

（广义）量子斯坦因引理的陈述确实间接依赖于相对熵的定义，因此我们选择如何形式化这一定义可能会导致语义上不同的最终定理。也就是说，我们对这个定义中的无用值是敏感的。

遵循MATHLIB中关于无用值的惯例，一个合理的定义方式是：

这样值总是一个有限的实数。这将使我们能够在证明过程中使用（非常支持的）实数。

如果我们没有采用这个版本的的定义，我们也可能无法捕捉到在第三节中描述的错误。通过使用扩展实数正确定义它，我们在方程操作中面临更大的数学困难，并真正捕捉到了完整的物理语义。

D. 其他数学障碍

另一个更技术性的问题是在寻找多个定义上的“钻石”时遇到的，其中一个对象从多个来源继承数据。对我们来说，这发生在矩阵从多个算子范数继承拓扑的情况下。Hermitian矩阵内积自然诱导了一个范数，而一个范数自然诱导了一个拓扑，但这个拓扑在定义上与来自矩阵元素级拓扑的拓扑并不相同。尽管用户可以证明这些是相同的，但Lean并不识别涉及一个的表达式也涉及另一个，因此，在定义内积的过程中需要额外的注意。

广义量子斯坦因引理涉及多个下确界和上确界，例如，最优假设检验率是使用对双元素POVMs的下确界来定义的。人类很容易理解这等价于对特定Hermitian矩阵集合的下确界，或者等价于一组（并不明显是Hermitian的）矩阵集合；下确界值可以被视为一个概率，一个实数，或一个复数（因为它是两个复矩阵的内积）。这些类型变化中的每一个都需要证明排序是兼容的，并且所有集合都是适当有界的（即下确界是有限的），这大大复杂化了证明过程。

E. 与其他物理形式化的比较

我们的工作并不是第一个探索在形式定理证明器中形式化物理的项目。mathlib 本身就有一个证明，表明 CHSH 游戏对于交换和非交换算子有不同的值，这是用 C*-代数的语言表述的。一些物理的形式化已经在 Isabelle 中被探索[40, 41]，但这些大多局限于较小的规模。有两个大型项目脱颖而出：PhysLean 库[42]开发了大量单独的物理结果，还有一个在 Rocq 中验证的 Shor 算法的实现[43]。

软件工程中有一条格言，即软件库不应该孤立开发，而应该针对特定应用进行开发；例如，Rust 编程语言的开发在很大程度上是由系统内开发一个网络浏览器的并行工作指导的。类似地，虽然 Lean-QuantumInfo 最初是关于量子信息的一组不相关的事实上，但专注于一个定理有助于形成一个连贯和综合的定理集合，包括所有必要的兼容性定理和谓词之间的关系，以便在不同领域之间移动。这类似于在验证的 Shor 算法[43]中采用的专注方法。

但我们方法最显著的不同之处在于努力验证一个新的、最近的结果，而不是标准的教科书定理。

V. 结论与展望

我们已经正式验证了文献[6]中所述的广义量子斯坦因引理的证明。导致广义量子斯坦因引理的步骤中的例外是量子信息理论中的一些标准结果，例如数据处理不等式。完成这些将得到一个端到端的证明。

据我们所知，这是使用Lean形式化物理中单个定理的最大努力。我们预计，这以及伴随的代码库[13]将促进Lean和形式化社区与量子信息社区之间的富有成效的合作。

从所示结果出发的下一步包括去除引理对其他经典定理（如数据处理不等式）的依赖，这些定理已被陈述为公理。证明这些陈述将大大提高用Lean编写的量子信息库的可靠性。

更直接适用于广义量子斯坦因引理的主题，将结果推广到非单位量子资源理论以及作为广义量子斯坦因引理的推论得出的结果（例如量子资源理论的第二定律）也很重要。

这项工作为量子物理和量子信息建立了一个正式化的基础，并通过证明一个特别且高度非平凡的定理来证明这个基础的可用性。除了标准的希尔伯特空间表述[39, 44–46]之外，还可以考虑量子信息理论的不同公理构造。例子包括广义概率理论[47–51]，以及C*-代数或冯诺依曼代数理论[52, 53]，后者可以应用于代数量子场论[54, 55]。所有这些方法都可以同时形式化，并从可互换和可扩展中受益。此外，还可以考虑受物理启发的方法，例如高斯量子力学、量子光学等。在Lean中正式化的量子信息的额外工作意味着结果和思想交流的有效且新的途径，类似于开源项目中的社区开发。

原文链接：https://arxiv.org/pdf/2510.08672