Aaronson-Ambainis 猜想：AI 用三天证明了一道 18 年未解的量子难题

11 月 6 日，一家名叫 Physical Superintelligence（PSI）的小公司宣布了一件十年前听起来像是科幻小说的事：一个 AI 研究系统——运行着一个未公开的 Anthropic 模型——证明了 Aaronson-Ambainis 猜想。这是量子复杂性理论的核心开放问题，自 2008 年以来一直悬而未决。系统在运行的第三天就得到了完整证明。Lean——逐一用机器检验每一步逻辑的证明助手——接受了它。PSI 随后让系统继续攻关相关问题，两次改进了结果，并发表了论文和公开的 Lean 形式化证明，任何人都可以重新检验这项工作。

要理解它为何重要，先从量子计算机真正擅长什么说起。1994 年，Peter Shor 找到了一种量子算法，能以远快于任何已知经典方法的速度分解大数。但 Shor 的加速依赖于一种罕见的天赋：问题本身隐藏着重复模式，而量子计算机能找出它重复的频率。已知的大多数惊人的量子加速都是这样运作的：它们利用结构。

Scott Aaronson 和 Andris Ambainis 提出了一个令人不安的问题：那随机输入呢？随机输入几乎从不具备这种结构。量子计算机能否以比普通计算机少得多的读取次数，回答关于一个随机字符串的是非问题？他们提出了一个关于多项式的猜想——纯数学——并证明，如果它成立，答案是否定的：在随机输入上，量子计算机至多快上一个多项式倍。这个猜想成了量子复杂性理论的核心开放问题之一；2026 年 8 月，一个斯坦福小组证明了它的一个特例：以固定轮数并行读取输入的量子算法。

PSI 的证明遵循 Shachar Lovett 和 Jiapeng Zhang 提出的方案，把他们方案中留作猜想的一个不等式，替换为论文中证明的一个新不等式，用的是基于 David Reimer 的蝴蝶引理（Butterfly Lemma）的配对论证，以及其他几个小组的结果。参与其中的人类——PSI 的 David Turturean——搭建了这个研究系统、界定了问题、运行了它，并对论文的正确性负责。顾问 Jim Halverson 审核了证明。证明了特例的斯坦福小组一直在阅读完整证明，提出了意见，正在为专家写一篇更简短的阐述。他们目前的评价是：“这是一个巨大的成果。”

这才是阅读这则新闻的正确方式——不是把它当作加冕，而是一项附带可检验成果的宣称。Lean 的接受是一个很高的门槛：一台机器已经验证了论证的每一步。Lean 无法检验的是，形式化后的命题是否就是数学家真正关心的那个命题，或者形式化过程是否偷偷带入了一个隐藏假设。这是人类专家的工作，而且尚未完成。同行评审还没有发生。找到这个证明的模型并不公开，所以没有人能重新运行发现过程本身——只能检查它产出的东西。

而这则公告所处的这一周，才是真正的故事。PSI 的证明不是孤立事件。10 月，OpenAI 发布了 722 篇 AI 撰写的数学手稿，其中包括对拟黎曼猜想、唯一博弈猜想和一类特殊形状的霍奇猜想的所谓证明。9 月，《数学季刊》上的一篇论文报告，一个 AI 系统找到了关键思路，把关于 k-微分的有条件结果变成了无条件定理，关键引理在 Lean 中得到了形式化证明。Axiom 则把约 7500 页的 Stacks Project——约 1600 万行——形式化了，使一大批代数几何成果变得机器可检验。模式已经再清楚不过：AI 提出证明，Lean 负责裁决。瓶颈已经从发现证明转移到了验证证明，而验证环节仍然由人类决定节奏。

我关注的正是这种转移。如果斯坦福的阐述顺利落地、没有其他小组发现漏洞，Aaronson-Ambainis 证明将成为一个月内第二项经受住专家审查的 AI 宣称成果——问题将不再是 AI 能否做前沿数学，而是验证流程能跟上多快。我的预测是：到 2027 年 12 月 31 日，这项证明将获得独立数学家的公开确认——通过斯坦福小组的阐述、同行评审期刊的发表，或等效的公开专家确认——且证明中未发现实质性漏洞。我给出的概率是 65%：机器层面的门槛已经跨过，合适的专家已经介入，但人类的确认不是走过场，一个定义的偏差仍可能让一个通过 Lean 检验的证明翻车。