PSI报告：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的多项式数量次查询，在大多数输入上对其进行模拟。这意味着，对于任意固定的近似误差和排除输入的比例，经典查询次数呈多项式增长，而非指数增长；但这并不排除在具有适当结构的问题中存在指数级量子优势。

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

证明的构建与验证过程

这一论证遵循Shachar Lovett和Jiapeng Zhang提出的方案，该方案以分数证书和水平集为基础；不过，PSI用一个新的全对不等式，替换了原方案中尚属猜想的一个不等式。一个行列式构造出输入配置之间的一一配对。PSI表示，这种配对优于David Reimer较弱的蝴蝶引理配对，因为它还限制了配对配置在各个坐标上相同的次数，而这一界限是新不等式成立所必需的。

该仓库将初等证明分为四个部分：从行列式和双射推导全对不等式；在水平集上对其积分；对各坐标取平均；以及通过逐点敏感度界建立行界。以上步骤共同得出了明确的影响力界。

根据该仓库记录的审计结果，形式化证明中没有占位证明，也没有添加公理。这些声明经过Lean内核和lean4lean（一种独立实现的Lean类型检查器）重新验证。在沙盒环境中，使用nanoda内核和Lean内核的比较器接受了最终的四个定理；在另一台机器上，它接受了一个正确的小型解答，并拒绝了四个故意写错的解答。

这些检查也有明确的局限。读者仍须确认形式化陈述与印刷版猜想相符。面向人类阅读的论文本身并未经过机器验证；此外，Lean内核和编译器、Mathlib的定义，以及用于验证的机器，仍属于可信计算基础的一部分。

人工参与者与专家评审

PSI技术团队成员David Turturean负责开发并运行该研究系统、界定问题范围、提示模型整理出初稿、审阅初稿，并对论文的正确性负责。该仓库披露，数学陈述、初稿和Lean形式化证明均由AI模型生成。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 之外的部分。这种分工决定了机器检查能够证实什么，以及哪些内容仍需由人类进行数学审查。