PSI 用非公开 Anthropic 模型给出 Aaronson-Ambainis 猜想证明，Lean 4 全量验证、无外部同行评议
2026 年 11 月 6 日，Physical Superintelligence（PSI）公布：其内部研究系统在自有基础设施上运行未公开的 Anthropic 模型实例，在第 3 天给出 Aaronson-Ambainis 猜想的完整证明，Lean 证明助手接受；随后系统被指派到相关未解问题，途中两次改进结果，最终版本再经 Lean 接受。数学论文与 Lean 4 形式化同步公开。
关键事实：
- 猜想本身：Aaronson 与 Ambainis 于 2008 年提出，问量子计算机在随机输入上能否指数级更快。Shor 1994 年的因数分解之所以指数加速，靠的是输入里的重复结构；随机字符串没有这种结构。两人把问题化归为多项式命题：若成立，经典算法可用 T 的多项式次查询在绝大多数输入上模拟 T 次量子查询。
- 证明口径：任取次数不超过 d、取值在 0 到 1 之间的多项式，方差为 v 时，某个坐标的影响力至少为 c·v^(5/2)/d^6，其中 c=8√15/(125π⁴)≈0.0025，也即不低于 (v/d)^7。此前一般多项式的界随次数指数衰减。路线沿用 Lovett 与 Zhang 的分层证书方案，把他们留作猜想的那个不等式换成新证明的全对不等式，配对由行列式生成，比 Reimer 的 Butterfly Lemma 多一条约束：成对赋值在每个坐标上一致的次数有上界。
- 验证手段：Lean 内核 + lean4lean（独立类型检查器）复跑声明，另有 Lean 与 nanoda 双内核的沙箱比对器接受最后四条定理；仓库审计记录显示无未证明占位符、无新增公理。局限一并在案：Lean 内核、编译器、Mathlib 定义与检查硬件仍在信任基内；机器只能确认「代码证明了这段陈述」，无法确认这段陈述就是原始猜想，论文的自然语言部分不经机器检查。
- 人的角色：David Turturean 开发系统、界定问题、跑系统、让模型起草论文初稿并复核，对论文正确性负责；两位 PSI 顾问 Jim Halverson 审计证明、Phiala Shanahan 复核形式化——审计由内部完成。8 月斯坦福 Blanc、Docter、Strassle、Tan 已证该猜想在并行轮数固定这一特例下的预测，他们随后读了全稿、提出意见并另写简版，评语为「This is a huge result」。
- 边界：不涉及因数分解，不对量子计算整体下结论；Anthropic 未置评，模型未具名。
观点
- 这次的分量在验证路径。机器可复核意味着任何人能自己跑一遍，与 10 月 27 日那份靠删节数据支撑的加速评估（#469《METR 独立评估：Anthropic 模型能力提升速度约为此前两倍》）正好互补：一份证据加密，一份证据公开。
- 形式化的边界必须写明：Lean 保证的是代码与陈述的关系，陈述是否等于学界关心的命题由人判定。这与 10 月 26 日 ETH 那次「形式化只覆盖弱一档主张」是同一类问题（#432《OpenAI 称模型证伪指数时间假设 ETH》），差别在 PSI 主动交代了覆盖范围与信任基。
- 三天出完整证明、再两次自我改进，是「模型产出可机器验收结果」最实的一个样本；它够不上递归自我改进的直接证据（模型未具名、无对照组、单例），但说明在可形式化领域，人类复核的瓶颈正被工具链接走。
- 产业读数很短：数学、芯片验证、编译器、协议这类本来就有机器可判验收标准的领域先受益；验收落在湿实验的生物与材料，同一套方法挪不过去。