量子 × 数学 · 指数从二十二降到七，关掉的是一条多数人本来就不信的路

十八年的一道题，第三天有了答案。答案是一块牌子，写着不用再往那边找了。

给你一本合上的书，规则是只准翻开若干页，看完就得合上，然后回答书里藏的某个是或否的问题。经典办法是一页一页翻。量子办法能把手指同时压在很多页上，靠干涉把答案读出来。2008 年 Scott Aaronson 与 Andris Ambainis 追问的是：如果这本书里的字完全随机排布，一个规律都找不到，压很多页还能省下翻页次数吗。十几天前，这个问题有了结果，结果说省不下。

11 月 6 日，初创实验室 Physical Superintelligence（PSI）宣布，自研研究系统跑一个未公开的 Anthropic 模型，在单次运行的第三天给出了 Aaronson–Ambainis 猜想的完整证明，Lean 证明助手逐步接受。系统随后又改进了两轮，最终版同样过了 Lean。研究页与 Lean 仓库同日公开，论文单作者是 PSI 的 David Turturean。11 月 8 日 Aaronson 在博客里回应，11 月 9 日 arXiv 上多了两篇后续论文，11 月 12 日中文媒体把这串事集中讲了一遍。中文报道里写的「搁置 18 年」，数的是 2008 到 2026。

猜想想找的那一页

早年 Beals，Buhrman，Cleve，Mosca 与 de Wolf 给出一条转换：一个读了 T 次输入的量子算法，它回答「是」的概率可以写成一个次数不超过 2T、取值落在 0 到 1 之间的多项式。于是「量子能不能更快」被搬进了布尔函数分析的语言，变成一个关于多项式的断言。

这个断言说：只要这样的低次多项式有明显起伏，就一定存在某一个输入变量，翻动它带来的平方变化在平均意义下足够大。这个量叫 influence，可以理解为「哪一页最要紧」。只要断言成立，经典算法就能先盯住那一页，把不确定性削掉一层，再对剩下的部分重复同一套动作，最后在大多数随机输入上用多项式次翻页逼近量子算法的答案。

Aaronson 与 Ambainis 2009 年首挂 arXiv 的论文《The Need for Structure in Quantum Speedups》（编号 0911.0996，期刊版见 Theory of Computing 第 10 卷，2014 年）证明了「如果猜想成立，会有什么后果」。猜想本身留了下来。中间有过一次翻车：2019 年 11 月 Nathan Keller 与 Ohad Klein 挂出一份证明，Aaronson 当时写了看好它的帖子，约两周后作者撤回，因为 Paata Ivanisvili 在其中一条引理里找出了致命漏洞。2023 年 Shachar Lovett 与 Jiapeng Zhang 给出一份进攻路线，把关键的一条不等式留成猜想。2026 年 8 月，Stanford 的 Guy Blanc、Jordan Docter、Carmen Strassle 与 Li-Yang Tan 解决了固定并行轮次的特例，论文被 FOCS 2026 接收，一般情形仍空着。

一个常数，和它后面那串指数

PSI 给出的主界可以写成这样：次数为 d、方差为 v 的有界非常数多项式，必有某个变量的 influence 不小于约 0.0025 乘 v 的 2.5 次方再除以 d 的六次方，这个界不小于 v 除以 d 的七次方。常数约 0.0025。论文附录 A 记着指数的三次变化，从 22 到 11 再到 7，每一版都过了 Lean。

那条补上的不等式来自一个行列式构造的配对，把输入设置一一对应起来，比 David Reimer 2000 年概率论证明里的 Butterfly Lemma 更强。它正好填进 Lovett 与 Zhang 路线留下的缺口。论文里的 AI 披露写得很直白：本文的数学陈述由 AI 模型产出；模型实例负责检索已有想法，提出新想法，把想法组合起来检验，还监督彼此的工作与通信。Turturean 负责界定问题，搭建并运行这套系统，让模型写出初稿，再审阅修改，论文写明他对手稿正确性负责。顾问 Jim Halverson 审了证明，Phiala Shanahan 看了 Lean 形式化。用的到底是 Anthropic 哪一个模型，PSI 与 Anthropic 都没有说。

机器签的字，和人还要读的部分

Lean 仓库里有一节叫「信任边界」，是这批材料里最该先读的文档。静态审计说四个最终定理没有 sorry，没有新增公理，也没有 native_decide，只依赖 Lean 的三条标准公理；Lean 自带的 leanchecker 把每条声明过了一遍内核，独立实现的 lean4lean 又重放了一遍，还有用 nanoda 内核做的沙箱比对。仓库按 Apache 2.0 放出。

同一节也列了机器没管的事。标着 PrintedConjecture 的那条形式陈述是否就是 Aaronson 与 Ambainis 当年提的猜想，留给读者确认；给人看的论文正文没有机器校验；Lean 的内核与编译器，Mathlib 里的定义，加上检查所用的硬件，都算在可信基里面。预印本尚未经过期刊同行评审。

Aaronson 11 月 8 日的表态也分两半。他写自己还没读懂这份证明，相信它正确有两个理由：有一份 Lean 证书，且人类专家已经通读并理解了它。他还写了一句「遗憾人类没赶在机器人之前拿下这个猜想」，并补上说再给几年，人类很可能也能做到。猜想提出者本人把信任放在证书与同行身上，这个姿态比任何一句「AI 攻克数学难题」都更贴近事实。

11 月 9 日，两份后续把证明摊开

验证链里最容易漏掉的是 11 月 9 日那两篇 arXiv 论文。

一篇是 2611.11626《Proof of the Aaronson-Ambainis Conjecture: An Exposition》，Stanford 那四位研究者写的释义，把证明整理成四个主步骤，讲清每一步与布尔函数分析、概率组合学文献的关系。作者注里说明，证明由 Turturean 用 PSI 的研究系统配合非公开的 Anthropic 模型发现，随后分享给他们理解与撰写；这个过程中用了 Anthropic 的公开模型；作者没有从 Anthropic 或 PSI 领取报酬；文章不打算投会议或期刊。释义明确说不优化参数，给出的指数比原证明弱。

另一篇是 2611.12795，v1 于 11 月 9 日 18:01 UTC 提交，7 页，Thomas Huffstutler 等人用 completion framework 给出一份短证明：定义在 δ 比例输入上的偏布尔函数，确定性算法可在其定义域的 1 减 epsilon 比例上，用与量子查询复杂度六次方成正比的查询次数算对。作者只借用了 Turturean 证书不等式的一个特例，并给了一份自洽证明，附录还从这个结果推出更强的有界多项式 influence 猜想。一份 18 年的猜想被证出后三天内出现释义与简化证明，这件事本身是学术共同体在接手，和「机器独自完成」是两种画面。

门关上了，屋里的东西没动

Aaronson 在 11 月 8 日的帖子里把边界划得很硬。这份证明不会终结量子霸权，也不改变量子计算机怎么造；对 Shor 分解算法的影响是零，对模拟量子物理与化学的影响也是零。它排除的是一类多数研究者本来就不相信存在的加速。Shor 能快，靠的是输入里藏着周期性，属于有结构的那一边。

还有两处限定得跟着走。结论针对大多数随机输入，并不保证每一个输入都能估准；数的量是算法读了多少次输入，总计算量另算。一次经典模拟即便查询次数不多，真跑起来也可能很贵。把查询次数当成墙上时钟，就会把这个定理读成它没说的话。

一个负向结果的价值就在这里。它告诉后来人哪条路不必再试，把力气留给还开着的那几条。11 月 12 日中文报道把它写成「AI 证明了量子计算猜想」，这句话少了一层：被证出的那条界约束的是多项式 influence，被关掉的是无结构输入上的指数查询优势，量子硬件的账单没有跟着变。

同一天还翻到

信源与限定：PSI 研究页 psi.inc/research/aaronson-ambainis/ 与 GitHub 仓库 physical-superintelligence/aaronson-ambainis（11-06 公开），单作者预印本 David Turturean，其 arXiv 编号未从本轮公开检索中核到，故不列；原猜想见 arXiv:0911.0996；Aaronson 博客 11-08 回应；arXiv:2611.11626 与 arXiv:2611.12795（v1 11-09 18:01:58 UTC）两篇后续；中文转载见腾讯新闻 11-12。Lean 仓库「信任边界」一节列出的机器验过与留给人类的项目按原文分列。常数表达式在不同二手源有两种写法，本篇只采用数值约 0.0025。结论的范围限于查询模型下、大多数随机输入、是或否问题，未涉及 Shor 算法与量子模拟。

#量子计算 #数学 #Lean #AIforMath #查询复杂度