导语
11月6日，美国初创公司物理超智能（Physical Superintelligence，简称PSI）宣布，其内部研究系统运行一款尚未公开的Anthropic模型，仅用三天就找到了Aaronson-Ambainis猜想的完整证明。这个自2008年提出、困扰学界18年的量子计算难题，由此可能迎来答案。PSI已将约60页的论文与Lean形式化证明一并公开在GitHub上，Lean证明助手逐项核验全部通过。
三天里发生了什么
按PSI的说法，研究系统在自家基础设施上运行，多个未公开Anthropic模型实例分工协作：检索已有思路、提出新想法、组合并检验这些想法、监督彼此之间的工作。运行到第三天，系统拿出了完整证明，Lean当即接受。随后，PSI又让系统去攻关几个相关问题，结果两次改进了证明，最终版本的指数从最初的22一路降到11、再降到7，每一版都经过Lean重新检验。
公开的形式化证明规模不小：84个Lean文件、761条声明、648个机器检验定理，没有留作占位符的步骤，也没有引入额外公理。PSI还用Lean内核与独立类型检查器lean4lean双重回放了全部声明，并在沙箱中用结合nanoda内核与Lean内核的比较器验证了最终的四条定理。论文的唯一作者是PSI技术人员戴维·图图雷安（David Turturean），他搭建并运行了这套研究系统、选定了问题、审读了草稿，并对论文的正确性负责。
证明思路建立在沙哈尔·洛维特（Shachar Lovett）与张嘉鹏（Jiapeng Zhang）提出的框架之上，核心工具是分数证书与水平集方法。原框架留有一个未被证明的不等式，AI系统的关键贡献是用一个基于行列式双射的新全对不等式替代了它，从而打通了整条证明链。
这个猜想到底在问什么
Aaronson-Ambainis猜想由得克萨斯大学奥斯汀分校的斯科特·阿伦森（Scott Aaronson）与拉脱维亚大学的安德里斯·安拜尼斯（Andris Ambainis）于2008年提出，核心问题是：量子计算机在什么条件下才能比经典计算机快出指数级？
猜想断言，每个有界低次多项式都存在一个高影响力变量。通俗地说，对于无结构输入上的判定问题，经典算法所需的查询次数只会随精度要求多项式增长，而非指数增长。换言之，在无结构数据上，量子计算的指数级加速是不存在的。但这并不排除另一面：对于具有合适结构的问题，指数级量子优势依然可能成立。
今年8月，斯坦福大学的盖伊·布兰克（Guy Blanc）、乔丹·多克特（Jordan Docter）、卡门·斯特拉斯勒（Carmen Strassle）与李阳·谭（Li-Yang Tan）已经证明了该猜想的一个特殊情形——固定并行轮数电路的情形，相关预印本将发表于FOCS 2026。据报道，这个斯坦福团队正在审读PSI的完整证明，并为专家撰写更简短的解读版本。
AI攻克数学难题的节奏正在加快
这不是孤立事件。就在十多天前的10月26日，OpenAI宣布其模型证明了计算复杂性理论中的重要假设“指数时间假设”不成立。两起事件相隔不到两周，指向同一种趋势：大模型正在从“辅助数学家”走向“独立发现证明”。
PSI本身是一家位于马萨诸塞州剑桥市的公益公司，自称“AI驱动的物理实验室”。值得注意的是分工：模型是Anthropic的、尚未公开，编排模型的研究系统是PSI自己的。也就是说，这次突破既不是某个公开模型的单打独斗，也不是传统意义上的人类数学家手工证明，而是一套人机协作的研究流程的产物。
对Anthropic而言，这也是一次意外的能力展示——一款尚未发布的模型参与攻克了悬置18年的难题，业界自然会好奇它的真实身份与能力边界。不过PSI没有透露模型名称，外界也无法直接使用它。
先别急着下结论：证明可验证，方法不可复现
尽管Lean已经为证明背书，仍有几个关键保留需要说清。第一，论文是预印本，尚未经过同行评审，学界的独立评估截至11月7日还没有发表。第二，人类可读的60页论文本身未经机器检验，Lean保证的是形式化代码中的定理为真，仍需数学家人工确认形式化表述与阿伦森、安拜尼斯的原始猜想完全对应。第三，猜想的提出者阿伦森本人截至11月7日尚未就此公开表态。
更深层的张力在于可复现性：证明本身是公开的，任何人都能用Lean重新检验；但找到证明的方法——未公开的模型加PSI内部系统——无人能够重复。这句总结很贴切：证明可以验证，发现过程无法复现。
如果斯坦福团队的审读与后续同行评审确认无误，这将成为AI数学研究的一个里程碑：机器不仅能验证证明，还能发现人类18年未能找到的证明。形式化证明工具与大模型的结合，可能正在成为数学研究的新范式——下一步，就看学界的审读结果能否让这个猜想正式从开放问题名单上划掉。