11月6日，初创公司 PSI（Physical Superintelligence）宣布，其内部研究系统在运行一款未公开的 Anthropic 模型时，证明了悬置 18 年的 Aaronson-Ambainis 猜想，完整证明在运行第三天写出，并通过了 Lean 证明助手的逐项验算。这是一次 AI 攻克数学难题的标志性宣称，但它目前还只是一家公司的说法——论文尚未经过同行评审。
这个猜想到底在问什么
Aaronson-Ambainis 猜想问的是：量子计算机在处理无结构数据时，到底能比经典计算机快多少？它断言，在无结构输入上，量子算法不可能实现指数级加速。这个问题自 2008 年提出以来一直悬而未决。今年 8 月，斯坦福大学一个团队先证明了一个特殊情形；PSI 称，自己的系统把结论推进到了完整情形。如果证明站得住脚，量子计算的能力边界就此划定了一条线。
机器是怎么证出来的，又查了几遍
按 PSI 的说法，研究系统在公司自己的基础设施上连续运行，第三天就写出了完整证明，随后又在相关问题上把结果改进了两次，Lean 每次都接受了最终版本。PSI 把论文和 Lean 4 形式化证明一并公开在 GitHub 上：648 个机器验算定理，没有留空的证明步骤，也没有额外引入公理；声明还经过 Lean 内核与独立实现的 lean4lean 双重重跑。PSI 技术人员 David Turturean 为论文正确性担责，另有数学家对证明做了审计。
先别急着把它写进教科书
机器验算通过，不等于数学界已经接受。Lean 只能保证每一步推导合规，无法确认形式化表述与 Aaronson 和 Ambainis 当年提出的猜想完全一致——这一点仍需专家人工核对；人类可读的论文正文本身也没有被机器验算过；证明计的是查询次数，而非总计算时间；所用模型也未公开，Anthropic 未予置评。同样在 11 月 6 日，谷歌 DeepMind 宣布 AI 智能体找到了 1024 位 RSA 加密的两处新弱点，AI 正在数学与密码学两个方向同时推进。PSI 的证明能不能经受住同行检验，未来几周的专家复核会给出答案。
