发生了什么
11 月 6 日，Physical Superintelligence（PSI）在官方研究页与 X 线程上宣布，其内部研究系统证明了 2008 年提出的 Aaronson–Ambainis 猜想。系统跑在 PSI 自有基础设施上，调用的是 Anthropic 未公开模型的实例。按其描述，完整证明在运行第三天产出，Lean 证明助手接受全部步骤；随后系统被调去处理相关开放问题，两次加强结果，最终版本同样通过 Lean 检查。
PSI 同时公开了论文与 Lean 4 形式化仓库。形式化部分以 Apache 2.0 发布，论文本身保留作者版权。仓库记录显示四条主定理均无 sorry 占位、未引入标准三公理之外的额外公理，并用 Lean 内核与独立实现 lean4lean 重放；另有一个同时调用 Lean 与 nanoda 内核的沙箱比较器验证最终四条定理，对照组接受了一个正确的小样例、拒绝了四个故意写错的样例。
这条猜想到底在问什么
1994 年 Shor 算法能指数级加速，前提是输入里藏着可被利用的周期结构。Aaronson 与 Ambainis 在 2008 年问的是反面：如果输入是一串均匀随机的比特、没有任何结构，量子计算机还能不能指数级领先？他们把问题转成一条纯数学命题——取值有界的低次多项式，必定存在某个影响度足够大的变量。若该命题成立，则在随机输入的是非问题上，经典算法只需多项式级的查询次数即可逼近量子算法的接受概率。
PSI 给出的界是具体的：存在某个比特，其影响度至少为常数乘以「方差的 5/2 次方除以次数的 6 次方」，常数约 0.0025，等于 8√15/(125π⁴)；也可粗略写作至少「方差除以次数」的 7 次方。此前同类通用界随次数指数衰减，这里换成了固定的七次方。路线沿用 Lovett 与 Zhang 的分数证书与水平集框架，但把该方案里仍属猜想的一条不等式，替换成一条用行列式构造一一配对后证明的全对不等式——PSI 称这一构造在限制配对项一致度上强于 Reimer 早年的 Butterfly Lemma。
机器验证到了哪一步
- 已验证：四条主定理过 Lean 内核、过独立类型检查器 lean4lean 重放、过双内核比较器交叉验证，并有拒绝错误样例的对照组。
- 未验证：论文正文本身不经机器检查；Lean 语句是否精确对应 2008 年论文的原话，需要人逐字确认。仓库为此专门留了一个只依赖 Mathlib 的定义 PrintedConjecture 供对照。
- 信任底座：Lean 内核、其编译器、Mathlib 的定义与检查用的硬件，仍在信任链之内。形式化通过不等于数学界认可。
换句话说，这份交付把「证明是否成立」从口头辩论变成了可重放的机器判据，但没有把「这串形式化语句是不是原猜想」一并解决。后者只能靠读定义的人。
人的位置，以及审计的性质
系统由 PSI 技术成员 David Turturean 搭建与运行：他界定问题、给模型下指令、审阅初稿，并对外承担论文正确性的责任。审计由两位顾问完成，Jim Halverson 审数学证明，Phiala Shanahan 审 Lean 形式化。这是内部审计，不是同行评议；截至 11 月 7 日，Aaronson 与 Ambainis 本人都未公开表态。
外部最接近评审的动作来自斯坦福的 Guy Blanc、Jordan Docter、Carmen Strassle 与 Li-Yang Tan：四人 2026 年 8 月解决过该猜想的特例，如今已读完完整证明并提交意见，正在为理论计算机科学家撰写一份更短的说明。历史提醒也不该省略——2019 年同一猜想曾有一次公开宣称的证明，后因漏洞被撤回。
对企业意味着什么
值得注意的不是「AI 又解了一道数学题」，而是交付形态：PSI 交付的是一份任何人都能重放检查的 Lean 工程，而不是一段博客结论。这与 11 月 6 日本站报道的 OpenAI 内核漏洞流水线是同一套工程思路——把「生成」与「校验」拆开，校验环节交给确定性工具。对需要为 AI 产出承担责任的团队，这是可复制的路径：产物必须自带可复核的判据，否则无法进入评审。
另一面是治理。用于发现的模型是未公开型号，Anthropic 未说明是哪一版、PSI 获得了什么权限，外部只能验证产物、无法复现发现过程。若这类研究成为常态，「结果可查、过程不可查」会成为采购与审计上的新常规，也是这类合作最难写进合同的部分。
不确定之处
结论限定在查询模型：它只约束「读取输入的次数」，不约束总计算时间，因此不能外推成量子计算整体没有优势；工程上真正被售卖的优势（采样、优化、量子模拟）多数不在这一模型的覆盖范围内。此外暂无期刊评审，形式化语句与原猜想的对应关系仍待数学界确认，PSI 自己的仓库也把这一步留给了读者。