PSI 报告 AI 系统给出 Aaronson-Ambainis 猜想的机器验证证明

Physical Superintelligence于2026年11月6日宣布，其内部研究系统运行非公开Anthropic模型的多个实例，已找到Aaronson-Ambainis猜想的证明，该猜想是自2008年以来悬而未决的量子计算问题。

该系统在PSI自有基础设施上运行的第三天产出了完整证明，Lean证明助手接受了该证明。随后，PSI将相关的开放问题分配给该系统，该系统两次改进结果，最终版本获得Lean接受。手稿和Lean 4形式化已公开。

该问题涉及量子计算机何时能比经典计算机快指数倍。Shor于1994年提出的因数分解算法依赖于结构：其输入带有算法可利用的重复模式。PSI的结果处理的是随机或无结构输入的对比情形，此类模式通常不存在。

在查询模型中，经典算法每次查询读取一个比特，而量子查询可以叠加态分布于许多输入位置。PSI的解释将该模型与多项式联系起来：经过T次量子查询后，算法回答“是”的概率是输入比特的有界多项式，其次数至多为2T。因此，模拟该量子算法就变成一个问题：如何在不读取指数多个输入比特的情况下估计该多项式。

在其原始论文中，Scott Aaronson和Andris Ambainis猜想，每个有界低次多项式都有一个高度有影响的变量。他们证明，假设该猜想成立，每个T次查询的量子算法在大多数输入上都可以由经典算法模拟，后者进行T的多项式次查询。其结果是，对于任何固定的近似误差和被排除输入的占比，经典查询数呈多项式增长而非指数增长；这并不排除具有适当结构的问题存在指数级量子优势。

在形式上，该仓库考虑一个次数至多为d的实多项式p，其在离散立方体上的取值介于0和1之间。如果其在均匀随机输入上的方差至少为ε，则某个坐标的影响至少为(8√15 / (125π⁴)) · ε^(5/2) / d⁶，因而至少为(ε/d)⁷。影响是指当该坐标的比特翻转时，p的期望平方变化。

该论证遵循Shachar Lovett和Jiapeng Zhang基于分数证书和水平集的方案，但将他们方案中留作猜想的一个不等式替换为一个新的全对不等式。一个行列式生成输入设置的一一配对。PSI表示，这种配对超越了David Reimer较弱的Butterfly Lemma配对，因为它还限制了配对设置在每个坐标上一致的频率，而这一界限是新不等式所需要的。

该仓库将这一初等证明分为四部分：从行列式和双射推导全对不等式，在水平集上对其积分，对坐标取平均，以及建立带逐点敏感性界限的行界。这些步骤共同得出显式的影响界。

根据仓库记录的审计，该形式化开发不包含证明占位符或新增公理。其声明已通过Lean内核和lean4lean（Lean类型检查器的独立实现）重放。在一次沙盒运行中，一个使用nanoda和Lean内核的比对器接受了四个最终定理；在第二台机器上，它接受了一个正确的小型解，并拒绝了四个故意错误的解。

这些检查有明确的局限。读者仍须确认形式陈述与印刷的猜想一致。人类可读的论文本身未经机器检查，而Lean的内核和编译器、Mathlib的定义以及用于检查的机器仍属于可信基础的一部分。

人类角色与专家评审

PSI技术人员David Turturean开发并运行了该研究系统，界定了问题范围，提示模型打包出初稿，审阅了该初稿，并对论文的正确性负责。仓库披露，AI模型产出了数学陈述、初稿和Lean形式化。Jim Halverson审计了该证明，Phiala Shanahan对形式化发表了评论。

该公告紧随Guy Blanc、Jordan Docter、Carmen Strassle和Li-Yang Tan于2026年8月19日提交的一篇论文。这些作者已经解决了并行量子算法的经典模拟推论，证明一个t次查询、d轮的算法可以在大多数输入上用t^(O(d²))次经典查询模拟。PSI表示，这四人一直在阅读完整证明，已提供评论，并正在为专家准备一份更简短的阐述。

在PSI发表的一份评估中，研究人员写道：“这是一个巨大的成果。它解决了一个数十年前的猜想，对哪些问题允许量子加速的本质具有重要影响。该证明借鉴并扩展了布尔函数分析和概率组合学中的若干研究方向。一切以相当神奇的方式结合在一起。”

直接的检验异常具体：独立内核可以重放编码后的论证，而专家仍须确认编码后的陈述与Aaronson和Ambainis的猜想一致，并评估论文中Lean之外的部分。这种分工决定了机器检查确立了哪些内容，以及哪些仍需要人类数学评审。