PSI 称其研究系统用非公开 Anthropic 模型证明悬置 18 年的 Aaronson-Ambainis 猜想，Lean 验证通过

2026 年 11 月 6 日，AI 物理实验室 Physical Superintelligence（PSI）在其研究页上宣布：一个由公司内部开发的研究系统，在 PSI 自有基础设施上运行一个非公开的 Anthropic 模型，找到了 Aaronson-Ambainis 猜想的证明。这一猜想由 Scott Aaronson 与 Andris Ambainis 提出，PSI 称其自 2008 年悬而未决，关乎量子计算机何时能相对普通计算机呈指数级更快。据 PSI 描述，系统在运行的第三天得出完整证明，Lean 证明助手接受了它；随后系统被转向相关开放问题，途中两次改进结果，最终版本同样通过 Lean 检查。

公告本身是公司单方口径：手稿与形式化都出自 PSI 自己的仓库，斯坦福研究者的评论也经 PSI 转述。能够公开核对的，是与公告同时放出的材料——论文手稿与一套 Lean 4 形式化已挂在 GitHub 仓库 physical-superintelligence/aaronson-ambainis 上，目前仍可访问。而就在今年 8 月，斯坦福大学的 Guy Blanc、Jordan Docter、Carmen Strassle 与 Li-Yang Tan 先解决了这个猜想的特殊情形；据 PSI 转述，这四位研究者称新工作是「a huge result」（一个巨大的成果）。

一次运行与一份贡献名单

运行中使用了非公开 Anthropic 模型的多个实例。页面的贡献栏列出分工：PSI 技术成员 David Turturean 领导这项工作——他开发了研究系统、选定问题、执行运行，再提示模型把结果整理成论文初稿，并审阅稿件、对论文正确性负责；顾问 Jim Halverson 审计了证明；顾问 Phiala Shanahan 对 Lean 形式化提出了意见。

PSI 官方 X 账号的公告帖还提供了一个背景：按其说法，上个月 PSI 已经解决了量子信息理论的五个长期问题。这一说法同样只出自 PSI 一方。

猜想问的是：量子加速是否必须依赖输入里的结构

1994 年，Peter Shor 找到了分解大数的量子算法，远快于当时已知的任何经典方法（arXiv）。它之所以快，是因为问题里藏着一个重复模式，量子计算机要找出模式重复的频率——PSI 页面指出，绝大多数已知的显著量子加速都依赖这类结构承诺：输入保证带有某种稀有模式。随机输入几乎从不携带这种结构；量子计算机在随机输入上能否指数级更快，此前没有答案。

Aaronson 与 Ambainis 把这个问题化成了一个纯数学命题。Beals、Buhrman、Cleve、Mosca 与 de Wolf 曾证明，量子算法 T 次「看」（查询）之后，其回答「是」的概率是输入比特的多项式，次数至多 2T、取值在 0 与 1 之间（arXiv）；普通计算机只要能少读几个比特就估出这个多项式的值，就能模仿量子计算机。两人据此提出一个关于这类多项式的猜想，并证明它若为真，量子计算机在随机输入上的加速至多是多项式级的。PSI 页面称，研究者一直把这一猜想列为量子复杂性理论的核心未解问题之一。

PSI 用一个比喻解释猜想本身：把多项式想成一块接在开关上的表盘，第 i 个开关是第 i 个比特的 0/1 取值，每组至多 d 个开关同时打开时，会给读数加上自己的正负份额，而读数始终落在 0 与 1 之间；量子计算机答「是」的概率就是这样一块表盘。猜想断言：只要读数在各个设置之间有方差 v，就总有某个开关，翻转它平均能让读数移动至少 v/d 的某个固定幂次——开关再多也一样。猜想成立意味着：在是/否问题上，除非输入藏有稀有模式，量子计算机省不下指数级的「看」。

这个猜想在两个多月前被解决了一个特殊情形。2026 年 8 月 19 日，斯坦福的 Blanc、Docter、Strassle 与 Tan 在 arXiv 发布《Quantum Speedups Require Structure or Depth》，证明任何 t 次查询、d 轮的量子算法，在多数输入上都能用 t^{O(d²)} 次经典查询模拟——用 PSI 页面的话说，对以固定轮数并行读取输入的量子算法，随机输入上不存在指数级加速。

证明沿 Lovett 与 Zhang 的计划补上遗留的不等式

PSI 页面说明，证明遵循 Shachar Lovett 与 Jiapeng Zhang 的计划（两人的 ITCS 2023 论文 Fractional Certificates for Bounded Functions）：对 0 到 1 之间的每个层级，考察读数不低于该层级的开关设置，并在每个设置上给每个开关分配权重，使翻转任何一组开关造成的读数变化不超过该组的总权重。Lovett 与 Zhang 把计划中的一个不等式留作猜想；PSI 的证明用一个新不等式替换了它，并在手稿中给出了它的证明。为证这个新不等式，证明把开关设置两两配对，配对由一个行列式产生——David Reimer 的 Butterfly Lemma（出自其对 van den Berg-Kesten 猜想的证明）给出的是较弱的配对，而新不等式还需要限制配对设置在每个开关上取值一致的频率。按页面所列，证明还用到 Avantika Agarwal 与 Shalev Ben-David、Raghav Kulkarni 与 Avishay Tal、以及 Yuval Filmus、Hamed Hatami、Nathan Keller 与 Noam Lifshitz 等人的结果。

按 GitHub 仓库中的表述，最终结果的精确形式是：离散立方体上次数至多 d、取值介于 0 与 1 之间的多项式，若方差至少为 ε，则必有某个变量的影响（翻转该位造成的读数变化的平方平均）至少为 (8√15/(125π⁴))·ε^{5/2}/d⁶，约等于 0.0025·ε^{5/2}/d⁶，且不低于 (ε/d)⁷。此前对一般多项式的界随次数指数衰减，那源自 Dinur、Friedgut、Kindler 与 O'Donnell 2007 年的定理；取值只有 0 和 1 的情形早已被 O'Donnell 等人与 Nisan、Szegedy 的定理覆盖，Montanaro、Ivanisvili、Bansal、Sinha 与 de Wolf、Escudero Gutiérrez 等人则先后证明过其他特殊情形。

手稿与 Lean 形式化已公开，其中一个定理带着未形式化的前提

GitHub 仓库 physical-superintelligence/aaronson-ambainis 在 11 月 6 日更新，包含论文 PDF 与一套 Lean 4 形式化，工具链为 Lean 4.33.0 与 Mathlib v4.33.0，代码以 Apache 2.0 许可发布。README 写明：四个定理均已证明，「无占位（placeholder）、无附加公理」，并已由两个相互独立的 Lean kernel（Lean 的核心校验程序）实现复查；其中主定理 aaronson_ambainis 对应的命题定义在只依赖 Mathlib 的 Conjecture.lean 文件里——按 README 的说法，读者只需核对这个定义，即可确认它证明的正是 Aaronson 与 Ambainis 论文《The Need for Structure in Quantum Speedups》中的猜想 1.7（即 arXiv 版的猜想 6，正式发表于 2014 年 Theory of Computing）。仓库还附有形式化指南、公理审计与验证笔记。

一个限定写在 README 里：第四个定理——把常数从 8√15/(125π⁴) 改进到 32√15/(125π⁴) 的版本——带一个前提 FbsDegreeBound，即 Agarwal 与 Ben-David 论文中的定理 1.7，这一前提本身未在仓库中形式化。README 的披露部分还写明：数学命题、论文初稿与 Lean 形式化都由 AI 模型在一个由 Turturean 在 PSI 开发的研究 harness（运行框架）中产生，Turturean 审阅论文并对其正确性负责。

一家成立两个多月的物理 AI 实验室

PSI 于 2026 年 9 月 1 日在马萨诸塞州剑桥成立，联合创始人为 Matt Pines（CEO）、Alex Klokus 与 Alexander Wissner-Gross，5,800 万美元种子轮由 Breakthrough Energy Ventures 领投（PR Newswire）。其官网称公司为公共受益企业（public benefit corporation），团队有 25 名以上的研究者与工程师，模式是「人类科学家指挥任务，虚拟物理学家执行研究」；首个产品化方向是把核心平台 Emmy 用于地面与轨道数据中心的设计优化，公司同时是私人资助的星际探测任务 Fermi Explorer 的创始技术伙伴。

外部反应与仍在进行的核对

过去几个月，AI 求解长期数学难题的消息接连出现。猜想的提出者之一 Scott Aaronson 在 9 月 15 日的博客文章中写道，「人类数学家作为这颗行星上主要定理证明实体的地位已被永久推翻」：他列举了 OpenAI 宣称在 Lean 中验证 Navier-Stokes 千禧年问题之解（此事伴随与人类数学家的署名争议）、Jacobian 猜想被称找到反例、费马大定理获得 Lean 验证的证明等近例，其中就包括斯坦福四人组对 Aaronson-Ambainis 猜想特殊情形的推进；同一篇文章提到，25 位菲尔兹奖得主（含 Terence Tao）已就「AI 在数学中的严重错位」发出公开信。

斯坦福四人组的评价由 PSI 转述刊出。按 PSI 页面登出的来信：「这是一个巨大的成果（a huge result）。它解决了一个数十年之久的猜想，对哪些问题能够获得量子加速这一本质问题有重要含义。证明汲取并延伸了布尔函数分析与概率组合数学中的多条工作线索，把所有要素以相当神奇的方式整合在一起。」四人已在阅读完整证明、向 PSI 发去评论，并为专家撰写更短的阐释文章。

在 X 上，公告帖截至 11 月 7 日获得 1,180 次点赞与 17.4 万次浏览。关注者约 9.4 万的账号 Hesamation把焦点放在模型上：「Anthropic 未发布的模型帮助研究者解决了量子计算中一个 18 年之久的猜想」，并写道「这些内部模型比公众能拿到的领先了多少，很有意思」。回复中也有直接的不信任：有人写道「猜想证明是一份契约：拿出形式论证，而不是公告」，还有人问「这是玩笑吗」。

PSI 官网写着它自己的验证标准：「当相互独立的验证形式汇聚到同一个结果上，它才成为发现。」眼下公开可见的核验材料——Lean 形式化、顾问审计、经 PSI 转述的斯坦福评论——都出自或经由当事一方。猜想的 Lean 表达就写在仓库的 Conjecture.lean 文件里，README 把它列为核对这份证明的起点。

参考链接

• PSI 研究页：A proof of the Aaronson-Ambainis conjecture
• GitHub 仓库：physical-superintelligence/aaronson-ambainis
• PSI 官方公告帖（X）
• Shor 算法原始论文（arXiv）
• Beals 等人量子查询多项式定理（arXiv）
• Stanford：Quantum Speedups Require Structure or Depth（arXiv）
• Lovett 与 Zhang：Fractional Certificates for Bounded Functions（ITCS 2023）
• Reimer：Proof of the van den Berg-Kesten Conjecture
• Aaronson 与 Ambainis：The Need for Structure in Quantum Speedups（arXiv）
• Agarwal 与 Ben-David 论文（arXiv）
• PSI 官网
• PR Newswire：PSI 成立与种子轮报道（Yahoo Finance 转载）
• Scott Aaronson 博客：The Age of Wonders and Terrors
• Hesamation 的推文（X）
• 用户 fishjar 的回复（X）
• 用户 Michael Dunworth 的回复（X）