纳维–斯托克斯与 Lean 证明：受迫奇点与实验室的不透明

2026年9月8日，OpenAI 宣称其一款从未向公众发布的内部模型，给出了三维不可压缩纳维–斯托克斯方程有限时间爆破的证明。公司公布了理论文档，以及公开代码库 NavierStokesAndEuler，其中包含用 Lean 4 语言写成的形式化定理：初值光滑、并受一个外部强迫项作用。按照该实验室自己的说法，这一结果覆盖了数学家查尔斯·费弗曼为克雷数学研究所起草的问题表述中关于正则性失效的命题，但并未处理没有外力的情形——而科学界普遍认为，后者才是这个问题更难的版本。官方表述的作者称这一结果令人振奋，并提到科尔多瓦与马丁内斯-索罗亚的贡献；与此同时，公司一开始就表明，无意申领那笔一百万美元的奖金。

这件事把数学的自动化与学术机构的时间节奏缠在了一起。克雷数学研究所仍将纳维–斯托克斯列为未解决问题：规则要求在合格刊物上发表、自发表起至少等待两年，并获得数学界的普遍接受，而研究所至今没有就实质内容表态。所长马丁·布里德森提醒说，评审刻意保持不慌不忙的节奏，以确保绝对的严谨。让局面更复杂的，是一场优先权争议：数学家陶哲轩介绍了一项同期进行的工作，其作者形容该工作在很大程度上借助了人工智能。纽约大学的一位数学家质疑了实验室对双方接触过程的描述，推测某个专有工具的私下会话可能对结果有所贡献；公司否认曾直接看到那份未发表的工作，但承认无法排除去标识化的使用数据对自家模型训练产生影响。

代码库给出了让机器复核该证明的操作说明，但迄今没有任何独立验证完成；而在这项检查之外，所用基础设施的专有性质，使得对其宣扬的成本和效率指标做任何独立核验都不可能。公布的算力——9月1日至5日间约一万个并发智能体，用88小时得到证明，再用17小时完成形式化与 Lean 验证——仍只是外界无法复现的企业陈述。既拿不到训练代码，也拿不到系统权重，科学界能够核验的只有代码库中提交的形式化步骤，实验真正的可复现条件仍留在阴影里。

形式化数学在逻辑步骤的自动检查中找到了强大的盟友，但以封闭模型争夺科学首创权，暴露出其结构性的限度。验证一条定理，如今已是机器可以完成的工作；而查清生成它的那条链条是否透明，仍然需要一种完全属于人类的严谨。

— Olya