近日，一家AI物理实验室证明了Aaronson-Ambainis猜想。这家实验室名为Physical Superintelligence（物理超级智能，PSI），成立时间很短，今年9月才亮相，专门用AI做物理研究。
Physical Superintelligence实验室公开了一篇长达60页的学术预印本论文《A PROOF OF THE AARONSON-AMBAINIS CONJECTURE》（Aaronson-Ambainis猜想的证明）。这一研究由PSI研究员David Turturean调用Anthropic未公开前沿大模型，在PSI的自建算力集群上运行仅3天，就完成Aaronson-Ambainis猜想证明。这一猜想困扰理论计算机科学界长达18年之久。
同时，整个推导过程完全通过定理证明助手Lean 4机器内核形式化审查，不留任何人工占位符，没有引入任何未经证明的外部假设。
虽然系统是人搭建的，问题是人选定的，但是证明本身完全交给了AI。甚至连猜想的提出者之一Andris Ambainis都发帖感慨，“我最大的几个科学难题里，又有一个被AI解决了”。
18年难题
量子计算的优势在于能够操纵量子比特的叠加态与纠缠态通过干涉效应抵消错误路径的概率幅，同时增强正确路径的概率幅。但是，这种加速并不是无条件的。量子算法的加速效能高度依赖于问题的“结构”
比如，大数分解问题本身是具有“周期性结构”的，所以1994年Shor算法能够实现对RSA加密的指数级破译。通过量子傅里叶变换（QFT），量子计算机能够绕过经典计算中低效的搜索过程，高效识别这种周期。
但如果不具备这种结构呢？早在1996年，著名学者Lov Grove就回答过了。
面对无序数据搜索时，相比经典算法，Grover搜索算法只能带来二次加速，也就是多项式级别的提速，如果经典计算机需要翻查一百万次，量子计算机则需要翻查一千次，而不是从一百万次降低至几次。
于是，一个困扰计算科学近二十年的的问题出现：在完全缺乏代数结构、没有预设约束的普通问题上，量子计算的加速极限究竟在哪里？它到底能不能在绝大多数普通输入上颠覆经典计算？
2008年，Scott Aaronson与Andris Ambainis，把这个关乎量子物理终极极限的命题，压缩成一道布尔代数分析难题，这就是著名的Aaronson-Ambainis猜想。
这一猜想的核心命题是，对于任何具有低阶多项式界限的函数，其是否存在影响变量？
他们断言：只要一个判定问题没有特殊的结构承诺，那么任何低查询开销的量子算法，在绝大多数输入实例上，其计算效果都可以被一台普通的经典计算机用类似规模的多项式查询开销完美复刻。
2019年11月，两位以色列学者Nathan Keller和Ohad Klein发布预印本论文，宣称攻克了Aaronson-Ambainis猜想。
不到一个月，佐治亚理工学院数学家Paata Ivanishvili在推演其引理时，发现了一个隐蔽且不可逆转的代数不等式错误。论文随即被作者主动撤回。
2023年，加州大学圣迭戈分校学者Shachar Lovett与Jiapeng Zhang引入布尔函数的分数证书复杂度理论，尝试通过几何凸包距离和极值理论绕开传统解析困难。
但是，他们最终卡在了自己构建的一个关于高维几何分离的不等式猜想上，不仅无法证明，后继研究更发现该几何假设在某些极端边界条件下根本无法成立。
传统的理论路径，似乎走进了死胡同。
多项式判定量子算力
2001年，Robert Beals等五位学者证明任何执行T次黑盒查询的量子算法，其最终接受某项输入的概率，都可以精确对应为一个关于输入比特的实数多项式，且该多项式的代数次数最多不超过2T。
这就意味着，衡量一个量子算法运行到底快不快、查询次数少不少，完全等价于观察这个概率多项式的代数次数低不低。量子算法如果跑得很快，那么，对应的多项式次数必然很低。
后来，Aaronson和Ambainis引入了度量指标“变量影响力”。在一个由海量输入比特控制的多项式中，如果单翻转某一个比特的取值，整个多项式的输出概率会出现明显的跳变，这个比特变量就被称为拥有高度的影响力。
基于此，Aaronson-Ambainis猜想预言，对于任何取值被限制在有限区间内、代数次数较低的非平庸多项式，无论它包含多少个输入变量，在它的全部变量中，必然存在至少一个变量，其影响力拥有一个不可逾越的非零下界。这个下界的大小与输入比特的总规模完全没有关联，只取决于多项式本身的方差和代数次数。
如果经典计算机要评估一个高效量子算法的输出，可以直接把算法拆解成对应的低度多项式。因为猜想断言必然存在一个影响力很大的关键输入比特，经典算法就可以先查询这个关键比特；确定关键比特后，整个函数的剩余不确定性就会大幅降低；接着，经典算法再去寻找下一个影响力最大的比特……
事实上，每查一步都在消解函数的方差，经典计算机只需进行多项式级别的查询次数，就能以极高精度逼近量子计算机的最终测定结果。
至此，证明量子计算机在无结构世界中无法实现指数加速，被彻底等价转化为证明“低度有界多项式必然存在高影响力变量”。
3天内完成证明
据PSI论文披露的技术细节，研究员David Turturean构建了一套“研究框架”：圈定命题边界、输入历史文献成果、搭建调度框架，且把算力环境接入到内部科研系统。具体推导、引理假设和跨学科工具的组合，全权交给模型在后端并发迭代。
在系统内部，分配了不同角色的智能体实例。比如，有的负责检索历史极值组合数学的冷门定理，有的负责构建反例检验，有的负责推导具体的不等式代数变形，还有的担任同行评审员，证明逻辑跳跃。
就在系统启动的第3天，大模型重新找到了一条纯代数分析路径，完全跳出Lovett和Zhang预设的高维几何凸包陷阱。
首先，系统放弃人为把函数切分为大于均值和小于均值的高阶硬性截断，转向引入连续全能级积分。通过对所有可能的临界能级引入阶跃水平集函数族，实现连续实数测度和离散空间分析之间的无损过渡。
随后，系统调用极值组合论中的Reimer不等式及其蝴蝶引理，甚至结合反极点矩阵变换，构造出对称消除恒等式。这一恒等式通过纯矩阵代数消元法，证明在任意两组点集之间都必然存在满足紧致放缩的代数匹配，这就避开了过去导致分析失真的测度长尾阻碍。
最终，系统推导出一个确定性的代数定量关系。对于任意代数次数较低且取值有界的多项式，其最大单变量的影响力下界，与函数方差的二分之五次方呈正比，与多项式代数次数的六次方呈反比，且与总变量规模脱钩。
未来可能还会有学者对多项式次数的衰减指数进行进一步的数学收紧，但是，对于计算复杂性理论来说，只要该下界和变量规模无关的多项式依赖关系牢牢绑定，在定性层面Aaronson-Ambainis猜想就已经宣告被全面攻克。
机器内核验算
众所周知，一篇60页的科研论文正常情况下都需要较长时间的同行评审，期间还会出现类似于2019年那样的隐形漏洞风险。但在这一次，PSI团队全程通过Lean 4的形式化机器审查完成，几乎让质疑者挑不出毛病。
作为当今最先进的交互式定理证明工具，Lean的底层逻辑基于依赖类型论。在Lean的语境中，任何自然语言中的跳跃、模糊语义或“显而易见”的人类习惯表述都会被剔除，每一个命题的成立都必须被拆解成机器内核能够直接执行的基础逻辑步骤。
PSI团队公布的Lean代码仓库非常清晰：从核心定理到所有支撑引理，完全闭环，没有留下任何人工标注跳步的占位符，没有调用任何额外的公理假设，甚至还使用了两套不同架构的独立Lean内核进行了交叉复核。
截至目前，PSI的这个成果还没有经过正式的同行评审，也没有外部团队完成独立验证。
但是，这一研究成果证明当下AI探索前沿科学的新纵深：它不再是生成可疑代码片段或辅助润色论文的工具，完成可以在与人类的智力竞争中脱颖而出，并自主打通一条严格的推导链路。
这也告诉我们，随着技术的不断演进，知道算力的边界到底在哪里，永远比盲目的技术崇拜更有价值。
[1]https://github.com/physical-superintelligence/aaronson-ambainis/blob/main/paper/aaronson_ambainis_paper.pdf
[2]https://psi.inc/research/aaronson-ambainis/
[3]https://blog.csdn.net/weixin_40774379/article/details/170236712
[4]https://abmedia.io/psi-anthropic-aaronson-ambainis-proof
