AI 三天证明 AA 猜想，十七年悬案落幕

图片来源：Hacker News · AI

11 月 6 日，量子计算初创公司 Physical Superintelligence（PSI）在官网宣布：一次运行进入第三天时，其自研研究系统给出了 Aaronson-Ambainis 猜想的完整证明，形式化验证工具 Lean 对每一步逐一核查后予以接受。据 Scott Aaronson 11 月 8 日在个人博客 Shtetl-Optimized 的文章，这套系统跑在 PSI 自建基础设施上，运行中调用了未公开的 Anthropic 模型实例；系统随后又两次改进结果，最终版本同样通过 Lean 检查。

运行第三天，Lean 收下证明

按 PSI 官网的贡献说明，系统由技术成员 David Turturean 开发，他选定问题、执行运行，再提示模型把结果打包成论文初稿，并对论文的正确性负责；顾问 Jim Halverson 审计了证明，顾问 Phiala Shanahan 对 Lean 形式化提出意见。论文与代码已放在 GitHub 上。据 Aaronson 回忆，PSI 团队早在数周前已私下告知他，他被要求保密至上周正式公布。数学结论是：对任何非常数的有界低次多项式，总存在一个变量，其影响度至少约为 v/d 的七次方（v 为方差，d 为次数）；用 Aaronson 博客的表述，即某个变量的影响度至少在 1/d⁶ 量级。11 月 9 日晚，这条消息登上 Hacker News 的 AI 板块，讨论从验证方法一路延伸到 Claude 的“感受”。

AI 生成的事件示意图，不代表新闻现场照片。

一道 2009 年立起的悬案

该猜想 2009 年由 Aaronson 与 Andris Ambainis 提出。它问的是：量子计算机在随机输入上回答“是/否”问题，能否比经典计算机指数级更快。借助 1998 年 Beals 等人的经典结果——T 次量子查询可写成次数不超过 2T 的多项式——两人把它化成关于多项式的纯数学命题，并证明一旦猜想成立，量子计算机在随机输入上最多只剩多项式级优势，同时回应了 1998 年 Fortnow 与 Rogers 提出的问题。

十七年里，傅里叶分析方向的学者与研究生把它当作主线课题，特殊情形的证明不断累积；2019 年出现过一版最终被证伪的尝试，Aaronson 在博客里记录过它的坍塌。2026 年 8 月，MIT 的 Guy Blanc 与斯坦福的 Jordan Docter、Carmen Strassle、Li-Yang Tan 解决了固定并行轮数的特例；PSI 的完整证明沿用 Shachar Lovett 与 Jiapeng Zhang 2023 年的路线，补上他们留下的一道不等式，再借 David Reimer 的“蝴蝶引理”与 Agarwal、Ben-David 等人的结果收束全篇。

AI 生成的事件示意图，不代表新闻现场照片。

“量子霸权死了”？Aaronson 逐条回击

消息扩散，误读随行。据 Aaronson 博客援引 Ashley Montanaro 的记录，华盛顿大学教授 Pedro Domingos 向其 13.7 万 X 粉丝宣布“量子霸权之梦已死”。Aaronson 的回应不留情面：新定理只排除了“相对随机谕示机的是/否问题”这一类本就少有人相信存在的加速；对 Shor 大数分解算法、对量子物理与化学模拟，影响为零；2022 年 Yamakawa 与 Zhandry 已证明，换成 NP 搜索问题，随机谕示机下的指数加速依然可能。博客评论区里，一个博士生领衔的小团队随即宣布，已把一份 5 页的自包含证明传至 arXiv。

数字跑腿，人来立问

被问及心情，Aaronson 给出四个词：满足——猜想为真；震撼；失望——人类没能抢在机器前面，“再给几年，他们多半能证出来”；以及疲惫，他说自己像守着阿拉丁洞穴的人，久违的开放问题正成批落地。另一位读者则在评论里写下了那个更冷的问题：当证明交由机器完成，数学家会不会“变笨”。

“这是一个巨大的成果。它解决了一个数十年的猜想……一切以相当神奇的方式汇聚在一起。”——Guy Blanc、Jordan Docter、Carmen Strassle、Li-Yang Tan，引自 PSI 官网

MIT 与斯坦福的四位人类学者正在撰写供专家阅读的简明阐述。据 Aaronson 博客，文章末尾的祝贺名单最后写着机器的名字——当然，还有 Claude。十七年前两位理论家立下的问句，如今由一套三天出活的系统作答，但圈定问题、审计证明、写下阐述的仍是人：机器跑得越快，人越要站在提问的位置上。