2008 年提出的 Aaronson-Ambainis 猜想，是量子计算理论领域挂了十八年的老难题。据海外科技媒体 11 月 7 日报道，一家名为 PSI（Physical Superintelligence）的研究实验室宣布，其内部研究系统运行 Anthropic 尚未公开的模型，在三天内找到了完整证明，并顺利通过 Lean 证明助手的逐行核验。这个猜想到底在讲什么、证明的可信度有多少、还剩哪些保留意见，这篇文章把它一次讲清楚。

十八年的悬案，三天有了答案

PSI 于 11 月 6 日在官网研究页发布了这项成果，论文与全部形式化代码同步公开，采用 Apache 2.0 许可证。整套工作由 PSI 技术人员大卫·图尔图里安（David Turturean）搭建的研究系统完成：系统跑在 PSI 自有基础设施上，内核调用的是 Anthropic 尚未公开发布的模型，具体型号没有披露。海外媒体向 Anthropic 求证时，对方未回应置评请求。

按照 PSI 的说法，系统在运行的第 3 天给出了完整证明，随后被转向相关开放问题，过程中又把结果改进了两次，最终版本同样通过了 Lean 检验。数学陈述、论文初稿和形式化证明均由 AI 模型生成，图尔图里安审阅了论文并对正确性负责。

这个猜想到底在说什么

先把猜想本身讲明白。量子计算机快，快在特定问题上：舒尔算法 1994 年就能把大整数分解做到远超已知的经典方法，但它依赖数论里的周期结构。于是问题来了——如果输入是完全随机的、没有任何结构可以利用，量子计算机还能不能指数级领先？

阿伦森与安拜尼斯在 2008 年的论文里，把这个直觉收敛成一条关于多项式的数学命题。此前的研究已经证明，量子算法对输入比特串做 T 次查询，其接受概率可以写成次数不超过 2T 的实多项式；猜想断言，只要这样的多项式不近似等于常数，就必然存在某个输入比特，翻转它会以可观幅度改变输出。这一条若成立，做 T 次查询的量子算法在绝大多数输入上都能被只花多项式次查询的经典算法模拟——换句话说，指数级量子加速必须来自问题本身的结构。PSI 给出的显式界是：度数为 d、方差为 ε 的多项式，必有某个比特的影响度至少约等于 0.00254 乘以 ε 的 5/2 次方、再除以 d 的 6 次方，正好落在猜想要求的量级里。

三天跑出证明，随后又改了两轮

这个速度对数学界来说相当陌生。2019 年曾有一版证明被阿伦森本人认可，随后就被同行找出关键引理的致命漏洞而撤回，前后不过数周。PSI 的证明沿用了洛维特与张佳鹏此前的路线，把该路线中原本被当作猜想使用的不等式换成了新证明的版本，同时吸收了赖默等人的既有成果。

按仓库披露，整份成果包含一篇 12 页论文和 84 个 Lean 4 模块、共 761 条形式化声明，四个主定理没有占位符，也没有引入额外公理。两个独立的 Lean 内核实现复验了全部声明，其中一次是从空环境开始，把 Lean 核心库与 Mathlib 数学库整体重查一遍。这套复现门槛，比绝大多数论文的可信度声明都要硬。

Lean 逐行核验，机器检查不是免死金牌

Lean 是一款证明助手，计算机逐条核对推理步骤，任何跳步都过不了关。这正是这份成果最扎实的部分：不管证明是谁写的，机器只认形式化之后能否通过。

不过机器检查也有边界。Lean 内核、Mathlib 的定义以及运行核验的硬件都在信任基础之内，人类可读的论文本身并没有被机器验证，还有一件事只能靠人：确认形式化文件顶部那 16 行定义，与阿伦森和安拜尼斯当年写下的猜想是同一件事。仓库把这一步做得尽量轻——读者只需核对一个名为 PrintedConjecture 的定义。

学界点头与悬而未决的审查

这项成果必须写明的一点是：它没有经过同行评审，也没有期刊发表。审计由 PSI 顾问吉姆·哈尔弗森完成，另一位顾问菲阿拉·沙纳汉对 Lean 形式化提出了意见，两人都是实验室内部顾问，因此审计属于内部性质。

外部信号目前是积极的。斯坦福的四位研究人员在 2026 年 8 月刚刚解决了猜想的特殊情形，他们正在阅读完整证明，并准备为专业读者写一份更简洁的说明；在反馈中他们称这是一项重大成果，认为它解决了一个对量子加速本质有重要影响的多年悬案。但非正式的通信不等于审查，学界进一步的独立核验仍需时间。

对普通用户来说，这个结果短期内不会改变任何产品体验——它讨论的是查询次数的渐进行为，界里的常数小到在具体问题里几乎碰不到，也不意味着量子计算贬值：利用问题结构的算法路线完全不受影响。真正的看点在研究范式：AI 生成、严格机器核验、人类担责的流水线，这次拿到了一个含金量足够高的样本。

网友评论

• 「三天干完数学家十八年的活，这效率放在我读书那会儿想都不敢想。」不少人对速度表示震撼，认为形式化验证补上了可信度这块短板。
• 「模型名字都不肯说，审计还是自己人做的，先打个问号，等独立团队复现再说吧。」也有网友对未公开模型和内部审计保持警惕，认为同行评审这一关省不得。
• 「求个通俗版解读：这玩意儿对我手上那些量子概念股有影响吗？」大概率没有，这次证明聊的是理论边界，不涉及任何在售产品。
• 「Lean 核验过就等于对了吗？定义要是抄错一行呢？」这个疑问很内行，仓库里专门留了一个人工核对入口。

总结

一次运行、三天、一个十八年猜想的完整证明，再加上 Lean 形式化和两轮自我改进，PSI 这次把「AI 做研究」的天花板又抬了一截。证明未经同行评审、审计来自实验室内部，这些保留意见应当与成果本身一起被记住。后续最值得盯的有两件事：斯坦福团队的独立解读，以及这种生成加机器核验的模式能否复制到更多学科。