AI三天证明悬而未决的量子猜想，机器核验，评论：只是符号死重

11月6日，Physical Superintelligence（PSI）宣布了一件事。其内部研究系统运行的是非公开的Anthropic模型，在运行第三天产出了Aaronson–Ambainis猜想的完整证明。

这个猜想从2008年起就悬着。它问的是量子加速的极限。在没有固定结构可循的问题上，量子计算机能不能比经典计算机快指数级。

验证方式值得单独说。证明提交给Lean证明助手，被接受了。之后系统两次改进结果，每一次都由Lean重新检查。PSI的仓库审计说，形式化里包含648个机器检查过的定理，没有占位符，也没有额外加公理。这些声明又用Lean的内核和独立检查器lean4lean回放了一遍。论文和Lean 4形式化文件都已公开。

机器验证有边界。人类数学家还得确认，形式化出来的陈述和Aaronson、Ambainis原来的猜想是一回事。文字论文本身没经过机器检查。模型不公开，三天的运行过程无法复现，能查的只有最终证明。

外面的反应分两头。有评论者认为，如果站得住，这是一个显眼的案例：AI在真做数学，不只是打下手。跟着的疑问是，当发现过程既不能查看也不能重跑、只有最终证明可查，数学的做法和信任方式会变成什么样。

也有人不认。一条高赞评论说，量子处理单元有更好的用法。另一条更实际：系统可以无限量吐出符号，没有人理解它，也没有人找到用法，这些符号就是压在资源上的死重。还有评论者明说自己是人类中心立场，主张禁掉机器人和先进AI研究，免得国家和物种失去存活的机会。

现在被机器逐条检查过的，是那份形式化里的648个定理。三天的运行过程不在其中。