三天证明一个悬了 18 年的量子计算猜想，用的是 Anthropic 一个还没公开的模型

一家叫 Physical Superintelligence（PSI）的物理实验室说，他们用 AI 在三天里证明了阿伦森—安拜尼斯猜想。

这个猜想 2008 年提出，问的是一个很根本的问题：量子计算机在什么条件下能大幅快过传统计算机。十几年来不少人试过，一直没有定论。

PSI 已经把论文和证明代码都放出来了，证明通过了 Lean 的形式化检验。Lean 是数学家用来让机器逐行核对证明的工具，过了它，至少说明推导链条在逻辑上没有漏洞。

之前研究过这个问题的斯坦福学者也读过证明并给了意见。不过学界的独立审查还没完成，现在说“已解决”还早了点。

关于工具：系统是 PSI 的技术人员大卫·图尔图里安自己搭的，跑在实验室的基础设施上，底层调用的是 Anthropic 尚未公开的模型。具体是哪个型号，没有说。

过去一年 AI 做数学的新闻不少，大多是竞赛题或者已知结论的重新证明。这次不同的地方在于，它是一个真实的、开放的研究问题，而且给出了机器可验证的结果。

如果审查通过，这大概会是 AI 参与理论计算机科学研究的一个标志性案例。