AI 系统三天证明一个悬置 18 年的量子猜想，Lean 形式化证明已通过校验

由 Physical Superintelligence（PSI）打造、运行着一个未公开 Anthropic 模型的研究系统，为 Aaronson-Ambainis 猜想给出了一份机器验证的证明——这是量子复杂度理论中一个自 2008 年以来悬而未决的开放问题。PSI 于 2026 年 11 月 6 日公布了这一结果，同时公开了一份 Lean 4 形式化证明。公司称，这份证明已通过独立的类型检查，没有任何未证明的占位符，除标准数学的基础公理之外也没有引入任何额外公理。

这个猜想最初由计算机科学家 Scott Aaronson 和 Andris Ambainis 提出，问的是：定义在布尔输入上的每一个有界低次多项式，是否必然至少有一个变量对输出具有高影响力。如果答案是肯定的——这份证明声称确立了这一点——那么每一个量子算法，在大多数输入上，都只需多花多项式级别的计算量，就能被经典计算机模拟。其含义十分明确：指数级的量子加速，要求问题的输入具备特定的代数结构。没有这种结构，量子计算机就得不到有意义的优势。

据 PSI 介绍，这个 AI 系统用了大约三天计算就完成了核心证明。随后团队又就相关问题向系统发问，引出了两轮指数改进，之后才对最终结果进行形式化和验证。经验证的影响力下界至少为 (8√15 / (125π⁴)) · ε^(5/2) / d^6，也可等价写成 (ε/d)^7——这是一个多项式关系，而此前的一般性下界会随次数呈指数衰减。

18 年的空白，以及两个月前出现的部分证明

Aaronson-Ambainis 猜想处在一个塑造了量子计算理论三十年的问题的中心：量子计算要想以指数级优势胜过经典算法，是否必须依赖有结构的问题？

Aaronson 和 Ambainis 在2008 年和 2014 年的论文中，把这一直觉形式化成了一个具体的多项式分析问题。在查询复杂度模型中——算法的复杂度以它读取输入的次数来衡量——Beals 等人早在 1998 年就已证明，对于全布尔函数，经典查询复杂度与量子查询复杂度之间总是存在多项式关系。这意味着，指数级的量子加速只可能出现在部分（承诺）函数上——也就是输入被保证满足某种全局条件的问题，比如 Shor 算法中的周期性。模拟猜想把这一直觉推广到低次多项式的情形，而 Aaronson-Ambainis 猜想正是它的具体表述。

18 年来，研究者只取得了有限的进展。2023 年，Shachar Lovett 和 Jiapeng Zhang发表了一套策略，把整个猜想归结为一个尚未证明的不等式。这套策略在其他所有方面都行得通——但唯独这一个缺口，即对所有布尔输入对求和的一个上界，顶住了每一次补上它的尝试。包括 David Reimer 的蝴蝶引理在内，标准的组合工具都不够强。

直到 2026 年 8 月 19 日，这个问题仍未解决。斯坦福的一个团队——Guy Blanc、Jordan Docter、Carmen Strassle 和 Li-Yang Tan——发表了一篇题为《量子加速需要结构或深度》的论文，证明了一个特殊情形：猜想的并行轮版本，即量子算法被限制为只进行一轮并行查询。这是实实在在的进展，但完整的猜想依旧悬而未决。这个斯坦福团队目前正在审阅 PSI 的完整证明，并准备一份面向理论计算机科学家的简短阐述。

AI 系统是如何补上这个缺口的

PSI 技术人员 David Turturean 搭建了这个研究系统，界定了问题范围，并在 PSI 的基础设施上运行它。系统拿到的是 Lovett-Zhang 证明策略，任务是找到一个能在现有工具失效之处奏效的不等式。

关键贡献是一个新的、基于行列式的配对不等式——严格强于蝴蝶引理。Reimer 的引理用组合论证来界定输入对上的求和，而 PSI 的 AI 找到的是一个基于矩阵行列式的上界，这个矩阵由输入对之间的一个双射构造而来，完整技术细节见PSI 的公开代码库。事实证明，正是这种方法补上了让整个 Lovett-Zhang 策略得以完整成立的那块缺失拼图。

完整证明分四步进行。第一步，运用基于行列式的不等式，借助双射构造建立一个全配对上界。第二步，把这个上界转化为在多项式水平集上的积分，把组合论证转换为连续形式。第三步，对所有坐标取平均，证明至少有一个坐标必须具有高影响力。第四步，用一个逐点敏感度上界确立完成影响力计算所需的行约束。这条推理链最终得出 (ε/d)^7 的下界。

这个 AI 系统并没有在第一份证明处止步。Turturean 就相关的开放问题向系统发问后，它在运行形式化之前两次改进了中间指数，最终得出了这个结果。这种行为——先生成一个有效证明，再自主把它收紧——与前沿 AI 系统在形式数学领域中越来越常见的那类后训练式精炼相一致。

PSI 的顾问 Jim Halverson 和 Phiala Shanahan 分别审核了证明本身和 Lean 形式化。两人都与 PSI 有关联，并非独立的外部审稿人——学界在评估这一公告时，会注意到这个区别。

Lean 验证意味着什么——以及不意味着什么

Lean 4 形式化，是 PSI 这一主张中技术上最重要的部分，而理解它的适用范围，对评估这个结果至关重要。

Lean是一个证明助手，会对照已声明的公理，机械地检查论证中的每一个逻辑步骤。只有当每一个中间结论都能从已确立的引理或公理推出时，证明才能在 Lean 中编译通过——不存在人类审稿人可能跳过或默认正确的空隙。PSI 报告称，完整证明先通过了 Lean 的核心内核，接着通过了lean4lean（一个对 Lean 自身内核进行再验证的独立类型检查器），最后还通过了一个使用 Lean 和 nanoda 两个内核的沙箱比对器，以验证证明的四个最终定理。

这是一项有分量的保证。此前也有 AI 生成的证明在没有形式化验证的情况下就被宣布，只能留给数学界手工审核——对于可能长达数百页的论证来说，这个过程既缓慢又容易出错。Lean 验证意味着任何人都可以独立运行检查：证明要么能编译，要么不能。

但 Lean 验证有其特定的适用范围。它确认的是：形式化的 Lean 代码证明了形式化的 Lean 命题。它无法确认这个形式化命题与 Aaronson 和 Ambainis 原本想表达的猜想完全一致。这被称为命题忠实度问题，需要人工审阅才能解决。PSI 那份供人阅读的论文并未经过机器检查；审稿人必须确认形式化的猜想与原始问题是同一回事。这项审阅仍在进行中。

可信基础还包括 Lean 的编译器、形式化数学库 Mathlib，以及运行这些检查的硬件——这意味着，即便内核接受了证明，这份保证在实践中仍有其边界。

这份证明为量子优势划出的边界

Aaronson-Ambainis 猜想成立的实际推论，是一个关于量子模拟的定理：每一个进行 T 次查询的量子算法，在大多数输入上，都可以被一个进行 T^O(1) 次查询的经典算法模拟。这就是模拟猜想，它也是Aaronson 和 Ambainis 提出这个多项式表述的最初动机。

这在实践中意味着：只有当输入问题具备量子算法可以利用的特定代数结构时，量子计算机才能实现指数级加速。周期查找——Shor 算法用于因数分解和离散对数问题的核心——恰恰就是这类有结构的问题。量子傅里叶变换之所以奏效，是因为输入被保证具有周期性；这种周期性，正是算法所需要的结构。

PSI 的结果并没有改变这一点。Shor 算法依然成立。后量子密码学的规划——其前提是，Shor 算法一旦在足够大的量子计算机上运行，就能攻破当前的公钥密码体系——不受影响。这一结果带来的是另一样东西：一个经过数学证明的下界，表明如果问题缺乏那种结构，量子计算机就无法获得指数级优势。

对量子计算行业及其投资者而言，这是对一条早已被理解的原则的细化——量子优势不是普遍的，而是结构性的——只不过现在支撑它的，是一份机器验证的证明，而不再只是专家共识。那些宣称在无结构问题上实现通用量子霸权的说法，如今面对着一道形式化的边界。

这个结果受限于它所采用的模型。查询复杂度模型只统计算法读取输入的次数，并把每次查询视为成本相同。真实的量子硬件涉及错误率、退相干和电路深度——这些都是查询复杂度没有刻画的因素。因此，模拟猜想的结论是一个关于查询访问的理论陈述，而不是对近期量子硬件能否在实践中胜过经典计算机的裁决。

一份等待同行评审、也在等待原提出者回应的证明

围绕这一结果，还有几个悬而未决的问题。截至 2026 年 11 月 7 日，这个猜想的提出者 Scott Aaronson 和 Andris Ambainis 都还没有公开回应 PSI 的公告。他们的评价分量格外重，既关系到数学界的看法，也关系到确认 PSI 的形式化命题是否抓住了原本想要解决的问题。在现阶段没有回应并不罕见，但学界会持续关注。

这篇论文尚未经过同行评审，也没有宣布投稿任何期刊。对于这样一个重大的结果——它终结了一个理论计算机科学界花了 18 年试图证明的猜想——由布尔分析和查询复杂度领域的专家进行独立同行评审，是这个领域所要求的标准。斯坦福团队的审阅和计划中的阐述提供了某种形式的专家审查，但并不能替代完整的同行评审流程。

如何为 AI 生成的数学贡献署名，这个问题也在演变。随着 Lean 验证成为 AI 辅助证明的标配，数学界开始要求在形式化证书之外附上溯源图——记录哪些步骤由 AI 生成、哪些由人类研究者提出，以及是否有任何关键步骤与此前未发表的工作相似。一些评论者呼吁进行完整的文献审计，要求每一份 AI 生成的证明都核实没有任何决定性步骤是从该领域现有的未发表工作中悄悄借来的。PSI 的披露中写明，David Turturean 是对论文正确性负责的人，这朝着学界开始期待的那种「由人负责」的署名方式迈出了一步。

PSI 这次的 Aaronson-Ambainis 公告，紧接着它2026 年 10 月 23 日公布的一批成果，那一次公司同时使用了 OpenAI 和 Anthropic 的模型，就五个量子信息开放问题发表了结果。不到两周时间里，PSI 已经拿出了六份声称解决开放问题的证明，全部经过 Lean 验证，全部有具名的人类研究者对正确性负责。这样的速度并不寻常。这些结果能否经受住完整同行评审的检验，将决定 PSI 这种 AI 原生物理研究模式——人类科学家指挥、AI 系统执行——究竟是一套可持续的方法论，还是一串需要学界花上数月才能评估清楚的早期成功。

对于这个具体结果，下一个里程碑很清楚：一份确认命题忠实度的审阅、Aaronson 和 Ambainis 的公开回应，以及一篇经过同行评审的论文。如果这三样东西到来时证明依然完好，Aaronson-Ambainis 猜想就将跻身已被形式化终结的问题之列——而悬置了 30 年的模拟猜想，也将随之得到解决。