当前位置：首页 > AI资讯

AI 三天证出搁置 18 年的量子猜想：数学圈被惊动

这猜想到底啥来头

结论先放：AI 这回不是在玩解题游戏，是真刀真枪碰了基础数学的硬骨头。Aaronson-Ambainis 猜想打 2008 年摆在那儿，讲的是量子查询复杂度里的一个边界问题，搁了 18 年没人彻底证出。PSI 的研究系统跑着一个非公开的 Anthropic 模型实例，第三天就交出了完整证明，而且 Lean 这个证明助手认了账。对咱外行说人话：有个形式化验证器点头了，不是嘴上说证完。米岸AI 看，这含金量比一般刷题高得多，因为形式化验证这关，糊弄不过去。

这证明靠谱吗

靠谱归靠谱，但得泼盆冷水。首先，这是内部审计式验证——PSI 说 Lean 接受了形式化，还有位顾问审计过，可没有同行评审，也没期刊发表。其次，用的模型是非公开的，外人复不了现。老程序员最懂这条：自家测试过了，不等于上线没坑。所以这成果目前是「内部确认 + 形式化通过」，离学术圈盖棺定论还差同行这关。咱看热闹可以乐，别急着写进教科书的序。

对象：Aaronson-Ambainis 猜想（2008 年提出）
用时：研究系统跑三天交出完整证明
验证：Lean 证明助手接受形式化
边界：无同行评审，模型非公开不可复现

AI 在科研里到底站哪格

这事儿不是孤例。前阵子谷歌 DeepMind 把药物发现压进一小时，Anthropic 自己的研发速度据 METR 评估快了近一倍，八成靠内部用 AI。AI 在科研里的角色，正从「查资料的小弟」往「能推导、能证伪的搭档」挪。但米岸AI 得说清楚：它现在更像加速器，不是替代物——最终拍板和兜底，还得是人。我带研发那会儿就明白，工具再猛，定方向、判对错的那个人不能缺。

为啥这事儿让数学圈警觉

数学圈怕的不是「被证明」，而是「被证明得太快、又看不太懂」。形式化验证能确认每一步推导合法，但一个非公开模型怎么想到的那条路径，外人无从复盘。这就好比有人甩给你一份全对的标准答案，却不告诉你思路——你信它能得分，却学不到方法。真正让学界安心的，是过程可复现、可教授。所以这一波惊喜里，也夹着一丝不安：如果发现的路径人类跟不动，知识该怎么传承？

对咱普通人啥信号

别一听「AI 证数学」就觉得科学家要失业。现实是，它能把人卡半年的死胡同快速试错、给出线索，省下的是重复劳动。真要写进教科书，还得人把关。咱看这事儿，乐见其成，但别神话——当年专家系统也吹过能取代专家，结果呢，不还是给人当工具。米岸AI 的判断：它是把科研的「草稿阶段」提速了，定稿阶段还是人的主场。