AI 系统正式攻克悬置近二十年的数学难题——这一幕在上周五成为现实。
AI 原生物理实验室初创公司 Physical Superintelligence（PSI）宣布，其内部研发系统在使用一款尚未公开发布的 Anthropic 模型作为底层的情况下，找到了 Aaronson–Ambainis 猜想的完整证明。该猜想自 2008 年提出以来一直是量子计算复杂性理论中的核心公开问题，探讨的问题是：量子计算机在什么条件下才能在随机输入上实现指数级加速。PSI 的证明给出的答案是设立了一个量子加速的基本上限。
这项工作的关键之处在于可信度：证明并非停留在纸面叙述，而是完整形式化为 Lean 4 证明助手可接受的机器检查证明。换言之，证明的每一步推理都经过了严格的形式化验证，不存在「AI 说自己证明了」的模糊地带。据多家媒体报道，该系统在三天内产出了完整证明，斯坦福团队已对结果进行了确认。
这个案例被广泛视为 AI 辅助数学研究的标志性事件：模型不是简单地检索已有文献，而是产出了一条能通过形式化验证的非平凡证明路径。对研究界而言，它同时提出了新的问题——当前沿模型开始解决公开数学难题时，形式化验证（如 Lean）正在成为区分「真结果」与「幻觉结果」的关键基础设施。
注：PSI（Physical Superintelligence）与瑞士保罗谢尔研究所（Paul Scherrer Institute）缩写相同，两家机构并无关联。