OpenAI 在最新公告里说,一套内部 AI 系统给出了三维不可压缩纳维-斯托克斯方程存在性与光滑性问题的证明,还配了一份 Lean 形式化验证代码。这是困扰数学界近九十年的千禧年难题之一。但公告里最耐人寻味的一句话,是"我们不打算申领这笔奖金"——这句自我克制,比证明本身更值得琢磨。
一边说解开了世界级难题,一边强调结果需要独立审查、不领奖金,这中间的落差,才是这次事件真正该看的地方。
证明说了什么
纳维-斯托克斯方程描述流体如何运动,是克莱数学研究所 2000 年列出的七个千禧年难题之一。问题很朴素:一团光滑起始的三维不可压缩流体,会不会在有限时间内突然"炸出"无穷大的速度?九十年来没人证明它一定不会,也没人证明它一定会。
OpenAI 这次给出的答案属于"会"这一支——他们构造了一个旋涡:向内旋转、被拉得越来越细,速度在有限时间内发散,但整个过程能量始终有限。这对应克莱官方问题清单里的C、D 两种情形,也就是"反例"方向,不是证明流体永远保持光滑。
结果包含两部分:一篇分析证明,和一份用 Lean 语言写的形式化验证。Lean 检查的是写进系统里的数学陈述和推导步骤是否自洽,不等于有独立数学家确认了问题设定本身没被简化,也不等于同行评议已经通过。克莱奖的规则是,结果要先在权威期刊发表,再等两年、没人反驳才算数——这一步,OpenAI 自己还没走。
规模是真的,含金量待定
8 月 28 日起,OpenAI 在训练一个新的内部模型,团队说它比"GPT-6 Astra"还要强——这次解题就是这个模型驱动的智能体在跑;等到最后的 Lean 形式化验证阶段,团队反而用回了 GPT-6 Astra 本身。这里顺带露出一个细节:反复出现的对照基准"GPT-6 Astra",此前并未见公开发布,公告像是提前给下一代模型打了个响指。
9 月 1 日,团队听到传闻说有人可能解出了两个千禧年难题,于是让系统同时尝试所有未解的千禧年难题。纳维-斯托克斯这一组用了约 1 万个并发智能体,88 小时后拿到结果,再花 17 小时完成 Lean 验证。过程中,agents 还顺手解开了一个更简单的版本——去掉粘性项的欧拉方程无外力光滑性反例,这直接促使团队把资源全部压向纳维-斯托克斯。巧合的是,Anthropic 员工 Levent Alpöge 和 NYU 数学教授 Tristan Buckmaster 也在同期公布了欧拉方程成果,但他们解的是"有外力"版本,和 OpenAI 的不是同一个问题,OpenAI 也公开承认了对方的优先权。
- 风险.智能体数量、消息数、token 数能说明工程规模,但不能直接证明数学论证没有漏洞——大力出奇迹在数学证明里从来不是自证清白的理由。
我更在意的是发布会和审稿之间的距离
历史上不是没有过类似争议。1976 年,Kenneth Appel 和 Wolfgang Haken 用计算机穷举证明了四色定理,当时也是"计算过程无人能逐行复核",数学界花了几十年才逐渐接受它,直到后来有人做出更简洁、可读的独立证明才算尘埃落定。计算机(或 AI)给出的证明,和被数学界签字确认的证明,从来不是一件事,中间隔的是时间和复核,不是公告。
敢证明,不敢领奖——这份克制里藏着几分心虚。
OpenAI 这次的克制,某种程度上是精明的公关:既拿到了"AI 能做顶级数学研究"的叙事,又不用真的承担"证明被推翻"的风险。公告反复强调的不是这道题本身,而是"内部模型比 GPT-6 Astra 还强""AI 进展的速度"——数学结果更像是给模型能力做的一次极限压力测试,顺手证明一道题算是彩蛋。
- 结论.真正决定这份工作分量的,不是 1 万个智能体跑了多少小时,而是接下来有没有独立数学家愿意逐行核对,并把它写进期刊。这一步现在还没有人做过。
接下来最该盯的,不是"AI 又赢了"这类标题,而是有没有具体数学家——尤其是研究纳维-斯托克斯正则性问题的专家——公开核对过证明细节。没有这一步,这份公告就只是 OpenAI 一个人的说法。