2026年11月6日，美国 AI 研究公司 PSI 宣布，其内部研究系统在一个未公开的 Anthropic 模型加持下，找到了 Aaronson-Ambainis 猜想的证明。这个量子计算理论问题自 2008 年悬而未决，系统在运行第三天就拿出了完整证明，证明助手 Lean 逐行检查后予以接受，随后结果又被改进两次，论文与 Lean 形式化代码已公开在 GitHub 上。
这个猜想到底在问什么
量子计算机最出名的优势来自 Shor 算法，能以指数级速度分解大数，但它依赖输入中隐藏的规律结构。Aaronson 与 Ambainis 在 2008 年问的是：如果输入完全随机、没有任何结构，量子计算机还能指数级更快吗？他们提出一个关于多项式的纯数学猜想，并证明一旦猜想成立，量子计算机在随机输入上至多比普通计算机快一个多项式倍数。PSI 的证明正是补上了这块拼图：它证明了普通计算机只需多项式次数的读取，就能以很小的误差预测量子计算机的回答概率。这意味着在是非问题上，没有规律可循的随机输入给不了量子计算机指数级优势。
机器验算通过等于定论吗
还不能这么说。Lean 的价值在于它用很小的核心代码逐行验证每一步逻辑，PSI 的形式化包含 648 个机器检查过的定理，没有留空步骤，也没有额外添加公理，两个独立的 Lean 内核实现都复核了最终的四个定理。但 Lean 只能保证写进代码的定理为真，无法保证代码里的表述与 Aaronson 和 Ambainis 原来的猜想完全一致，这一步仍需数学家人工确认；60 页的人读版论文本身也没有经过机器检查，更没有同行评审。斯坦福大学今年 8 月证明了该猜想特例的团队正在审读这份证明，并给出了积极评价，但两位猜想提出者截至 11 月 7 日尚未公开表态。PSI 的模型也没有公开，别人无法重复这次三天的运行。
对 AI 研究来说，这件事的意义不在量子计算本身，而在方法：一个内部研究系统在三天内走完了从提出思路、组合已有成果到产出可机器验证的证明的完整链条。今年 10 月 OpenAI 也曾公开 722 篇 AI 生成的数学手稿，同样要靠 Lean 形式化来核验。AI 写证明正在从猎奇变成可检验的工作流，下一步要看独立数学家的复核结论，以及这种系统能否在别的难题上复现。
