AI 参与量子计算猜想证明：Lean 检查覆盖到哪里？

一个关于量子加速边界的长期猜想，近日有了 AI 参与生成的形式化证明。Physical Superintelligence（PSI）11 月 6 日表示，其内部研究系统使用一个未公开的 Anthropic 模型，得到 Aaronson–Ambainis 猜想的证明；研究方称证明已由 Lean 接受。

这个猜想可以追溯到 2008 年。它关心的是量子计算何时可能比经典计算快得多：提出者把问题转化为关于布尔输入上低次数多项式的命题，并指出如果该命题成立，随机输入上的量子加速有相应限制。这不意味着量子计算没有用，也不能把它概括成“所有问题都不能有指数加速”；某些有特殊结构的问题仍需另行分析。

按照 PSI 的说明，系统在运行的第三天得到完整证明，之后又改进了结果。研究方公开了论文和 Lean 形式化材料；材料说明，主要形式化定理没有证明占位符，使用的是 Lean 数学库中的标准公理，并称使用两种 Lean 内核实现重放了检查。

机器检查的边界同样值得看：形式化命题是否准确对应原猜想，仍需要熟悉问题的人核对；面向读者的论文并非每段都与机器检查内容一一对应。材料还指出，一项更强的结论依赖一个尚未在该项目中形式化的前提。

因此，现阶段可以说研究方公布了一个经其机器检查的形式化证明方案；它是否被更广泛的数学界接受，还要看后续独立复核。这里没有自行运行证明，也没有把发布方的结论当作已经完成同行评审。