近日，OpenAI对外宣布其内部一个尚未发布的模型解决了纳维-斯托克斯方程的存在性与光滑性问题。这不是一道普通的数学题——它是克莱数学研究所在2000年提出的七个千禧年大奖难题之一，每道悬赏100万美元，二十多年里只有庞加莱猜想被攻下过。消息一出，数学界和AI圈同时炸了。
按照OpenAI自己的说法，这次不是人带着模型算，而是把问题交给了约1万个AI智能体并行推进。它们跑了大约88小时，互相发送了约270万条消息，消耗约1300亿输出token。结论指向一个反直觉的方向：一个初始光滑、静止的三维不可压缩流体，在施加外力后可以在有限时间内产生奇点，也就是速度在有限时间内无界增长，而动能始终保持有限。这个结论对应克莱官方问题陈述里的C和D两部分——反例命题。证明随后被送进Lean做形式化验证，每一步都能机器检查，配套论文166页。这里要分清两个角色：发现证明的是那个未公开的内部研究模型，Astra只负责把它形式化和检查，用时约17小时，它并不是解题的那一方。
这里有个容易被忽略的技术边界，不少中文转述都略过了。OpenAI解决的是“带外力”情形下的爆破，而克莱问题里更受关注的一般情形——不施加外力的三维纳维-斯托克斯全局正则性问题——仍然开放。这意味着，宣布的构造并没有把整个千禧年问题关掉。看新闻时把这一点分清，能避免很多误读。
克莱数学研究所9月11日发的公告值得逐字读。全文四段，绝大部分在讲这些奖项为什么存在，真正表态只有一句：“今天我们与全球数学界一同期待，纳维-斯托克斯问题似乎已被解决。”措辞克制到几乎冷淡：没有点名OpenAI，没有点名任何数学家，也没有启动奖金流程。该机构官网这道题的状态至今仍写着“Active”。原因在其规则里——候选方案必须在合格期刊发表，然后经受全球数学界至少两年的严格检验，再由特别顾问委员会评审。克莱主席Martin Bridson对媒体表示：“评审过程刻意不慌不忙，我们会确保它绝对严谨。”
证明本身也在被独立检验。据技术社区整理的进展，这份Lean项目已完成四次完整构建，覆盖两台机器和同一个固定提交，其中一次从源码编译了全部8370个mathlib模块，耗时约3小时13分，四次全部正常退出且输出一致；两个独立内核（Lean自带的，以及用Rust实现的nanoda）都接受了这套证明，与Google DeepMind的独立形式化在定义层面逐字节吻合，只差21处包装代码。质疑也同样具体：有研究者指出，形式化代码里“力的紧支撑”这一条出现在候选属性清单中，看起来是被当作前提假定的，而标注为待解决的那一处恰好是核心的存在性内容——若这一点没有真正得到证明，结论实际说的是“若存在这样的强制奇异解，则……”，并不足以直接对应千禧年问题里需要被反驳的两种情形。提出质疑的人强调自己并未判定结论有错，只要求把逻辑状态说清楚。这场讨论仍在进行。
围绕成果归属，已经出现两种说法。纽约大学数学家Tristan Buckmaster与在Anthropic任职的Levent Alpöge合作近一年，据称在8月15日拿到关键的欧拉与Boussinesq结果，8月22日首个AI生成证明通过Lean验证。Buckmaster称，他曾被OpenAI研究人员提出把Alpöge从可能的论文署名中剔除，理由是其在竞争对手任职；对方否认了这一说法，但为一句关于“毁掉职业”的发言道歉。OpenAI则表示内部调查确认其模型未受两人先前工作的影响，并说明自己的行动始于9月1日听到传闻之后。双方各执一词，支撑调查的材料和完整的智能体日志都未公开。
另一条线同样重要：就在克莱发公告的前一天，25位菲尔兹奖得主联名签署声明，警告AI公司之间围绕数学难题的竞争可能损害这门学科本身，签署者包括陶哲轩、Manjul Bhargava和Maryna Viazovska等人。陶哲轩用了一个形象的比喻——用挖掘机去考古遗址取宝，宝物或许到手，但让它产生意义的上下文被一并破坏了。OpenAI已经表示不打算申领这笔奖金。给技术从业者的提醒很实在：形式化验证能证明“结论对不对”，证明不了“过程有没有意义”。当一个答案可以绕过理解被直接产出，怎么评价、怎么归属、怎么让后来人还能学会，这些问题的难度不比原题低。
A5创业网 版权所有