OpenAI在官网博客里说,它内部一个模型调集了大约一万个并发智能体,花88小时给出了纳维-斯托克斯方程的有限时间奇点证明——这是七个千禧年数学难题之一,克莱数学研究所悬赏一百万美元,悬置了近90年没人解开。证明出来后,又花17小时用Lean把它做了形式化验证。

听起来是数学史上的大新闻。但博客里有两处细节经不起细看:文中提到的对照基线模型叫“GPT-6 Astra”,这个名字从未公开发布过;文中标注的关键时间只写了月和日,没写年份。这两处疑点,比证明本身更值得先划一道问号。

OpenAI证明了什么,没证明什么

纳维-斯托克斯方程把流体当连续介质处理,用来算天气、算血流、算飞机绕流,不追踪单个分子。90年悬而未决的问题是:流体速度会不会在有限时间内变得无穷大。一旦真的无穷大,连续介质模型在那一刻就失效了。

OpenAI自称证明的场景是:一团初始静止、总能量有限的流体,在光滑外力驱动下,内缩出一个越拉越细的涡旋,速度在有限时间内发散。

官方情形外力条件结论方向OpenAI证明是否涉及
A无外力光滑解永远存在未涉及,仍开放
B无外力(周期边界)光滑解永远存在未涉及,仍开放
C有光滑外力解会在有限时间破裂声称已证明
D有光滑外力(周期边界)解会在有限时间破裂声称已证明

也就是说,这次证明成立与否,跟“没有外力的自然流动会不会自发爆破”这个更常见、也更受关注的A、B情形,目前没有直接关系。哪怕C、D被最终确认,A、B依然悬着。

“奇点”这个词在这里的意思很窄:速度在有限时间内无界,数学模型失效,不代表现实里的水或空气真的能跑出无穷大速度。真实流体受粘性、湍流耗散这些物理机制约束,根本不会去验证这个数学极限。

这套证明动用了大约一万个并发智能体,88小时给出证明,另外17小时完成Lean形式化;仅纳维-斯托克斯这一项,官方博客给出的输出token消耗约1300亿。

证明速览:几个数字 10000+ 并发智能体 协同工作 88小时 得出证明 首批智能体启动起算 17小时 Lean形式化 验证证明步骤 1300亿 输出token 仅NS问题一项

Lean形式化能担保什么

Lean能挡的是证明步骤里的逻辑漏洞——每一步推导是否严密,机器可以逐句检查。Lean挡不住的是:证明的命题表述是否精确对应克莱官方问题、命题到形式化系统的映射有没有偏差、整套形式化框架本身有没有系统性问题。这些只能靠数学家逐行读原始论证,机器检验代替不了同行评审。

机器算得快,不代表算得对。OpenAI自己在文中也说不打算申领千禧年大奖——这句话等于承认,这份证明还没走到“被数学界确认”那一步,目前也没有第三方渠道显示克莱数学研究所已经受理或认可这项成果。

1989年那场轰动一时的“冷聚变”发布会是个提醒:先开发布会、后被同行推翻,代价从来不小。这次OpenAI多了一层机器可查的Lean代码,比当年多一道保险,但“先宣布、后审查”的顺序没有变——不完全一样,但值得警惕的地方是同一个。

接下来该看什么,对谁有影响

数学界要审查的东西很具体:原始证明文本是否公开完整、Lean代码仓库能否独立复现编译、C/D命题到形式化陈述的映射是否精确、有没有数学家公开发表审查意见。这几项都还没有公开落地。

关注前沿模型能力的技术读者,不要把“一万个智能体+88小时+1300亿token”直接读成“AI已具备自主开放性科研能力”。这更像一次资源密集型的能力展示,真正的能力信号要等复现结果和独立审查出来后再评估——暂时别把这次结果写进模型能力对比的基准里。

关心证明可信度和同行评审机制的科研从业者,现阶段能做的是核对官方博客链接的证明文本、Lean仓库和发布时间戳是否完整可查,留意是否有数学家在预印本平台或公开渠道给出具体审查意见,而不是等一份新的通稿来确认这份通稿。

【锐评】证未经审,先声已扬。千禧难题这块金牌,OpenAI现在还只是把它举起来看了一眼,离揣进兜里,差的是数学界那一句“对”。