一个悬了十八年的量子计算猜想，被 AI 系统证出来了，三天，外加 Lean 逐步验证

先交代这件事里确定的部分：PSI 在自己的研究页面上写明，系统跑在公司自己的算力上，用的是“一个非公开的 Anthropic 模型”的多个实例，运行到第三天就有了完整证明；随后他们让系统继续研究相关问题，期间系统把结果又改进了两次，最终版本被 Lean 接受。论文和证明代码都放在 GitHub 上，下面的来源里有链接。

01这个猜想在问什么

1994 年 Peter Shor 发现，量子计算机分解大整数比已知的任何普通算法都快得多。原因是这类问题里藏着“重复出现的规律”，量子计算机擅长找出规律多久重复一次。

Scott Aaronson 和 Andris Ambainis 想问的是反过来的情形：如果输入是随机的、没有任何规律，量子计算机还能不能指数级地更快？他们把这个问题转成了一条纯数学猜想，说的是某类多项式里，总有一个变量对结果影响不小。只要猜想成立，就能推出：面对随机输入，量子计算机最多只能比普通计算机快“多项式倍”，不可能是指数级。

PSI 页面里的比方是：把多项式想成一块表盘，每个输入位是一个开关，读数始终在 0 到 1 之间；猜想保证，只要读数不是一成不变，就一定有某个开关拨一下，读数会明显变化。普通计算机沿着这些“影响大的开关”一个个去看，看到剩下的开关影响很小就可以停手，由此模仿量子计算机的答案。

02“证出来”和“被验证”是两回事

大模型写出来的数学证明，过去常见的问题是看着像、其实有漏洞。这次的不同在于用了 Lean：它是一种证明助手，计算机会检查每一步推导是否合规，通不过就不接受。PSI 称最终版本通过了 Lean 的检查。

不过要分清楚：Lean 能保证形式化的证明链是对的，但“这条形式化陈述是否真的就是原猜想”，仍然要靠人来审。PSI 页面说明，Jim Halverson 作为顾问审了证明，Phiala Shanahan 评论了 Lean 形式化部分；论文由项目负责人 David Turturean 对其正确性负责。斯坦福的 Guy Blanc 等人今年 8 月刚在一个特殊情形下证明过同类结论，他们在读完整证明后评价为“很大的成果”，并在写一份给专家看的简短说明。这是 PSI 页面转述的评价，独立的同行评审还没有结果。

03对量子计算意味着什么

按 PSI 的说法，这意味着对随机输入的“是/否”类问题，量子计算机省不出指数级的“查看次数”，量子优势只会出现在输入带有罕见规律的场合，Shor 算法就是这种。这个结论并不否定量子计算的价值，只是把它的优势范围划得更清楚。社交平台上有人写成“量子计算泡沫破灭”，这是转述者的解读，官方页面没有这样说，原文最后一句是“量子计算还有很多谜，现在少了一个”。

还有一个细节值得留意：模型是“未公开”的，PSI 没说是哪一个，也没公开系统的具体构造。所以这个成果能不能被别人复现，目前没法判断。