据10月15日报道，OpenAI 宣布，由 10000 个 AI 智能体组成的集群，用 88 小时、消耗 1300 亿 Token，攻克了七大千禧年难题之一——纳维-斯托克斯（Navier–Stokes）方程的有限时间爆破（finite-time blow-up）问题。据报道，其证明代码已通过 Lean 4 形式化证明系统核验。

先补充一点背景：纳维-斯托克斯方程是流体力学的核心方程，描述粘性流体的运动规律，其解的存在性与光滑性问题是克雷数学研究所悬赏的七大千禧年难题之一，任何“攻克”声称都注定引发学界地震。

## OpenAI 的说法

按 OpenAI 的宣布口径，这是 AI 智能体集群首次在形式化验证的意义上“解决”千禧年难题级别的数学问题：大规模智能体并行探索证明路径，Lean 4 则保证了最终证明在逻辑上的严密性。形式化验证本应是这类争议的“终结者”——机器检查过的证明，不服不行。

## 剑桥方面的质疑

但剑桥方面对这一成果提出了质疑：其代码与论文内容对不上。也就是说，形式化证明系统验证过的代码，与论文中描述的数学论证之间存在不一致之处——这直接动摇了“已被证明”的说法。验证过的代码是一回事，论文声称证明的定理是另一回事，两者脱钩，验证本身也成了争议的一部分。

## 一点观察

这场争议恰好卡在 AI for Science 最敏感的位置：在双方拿出可复现的完整材料之前，建议读者把“攻克”二字先打上引号。无论最终结论如何，这件事都给行业提了个醒——形式化验证只能保证“代码逻辑自洽”，保证不了“代码证明的就是论文里写的那个定理”。

来源：http://k.sina.com.cn/article_5952915720_162d2490806704zymw.html