OpenAI把流体力学写进了Lean：一周783星，形式化证明到底在解决什么问题

先说结论

OpenAI 上周放出的 NavierStokesAndEuler 仓库，本质上是一份用 Lean 写的“证明证书”，对应的是流体力学里两个最让人头疼的方程——纳维-斯托克斯和欧拉方程。它一周拿到 783 颗星，热度不来自“AI又破纪录”，而来自数学圈对“形式化验证”这条路线越来越认真。

这件事离普通用户很远，但它回答的问题很实在：当一个数学结论号称被证明时，能不能让计算机自己检查一遍，而且这次检查不靠运气、不靠审稿人心情。

真正的问题

流体力学方程难，不是因为公式复杂。真正的难点在于它的“行为”——会不会在某一点突然产生奇点，会不会数值爆炸，会不会和物理对不上。过去一百多年，顶尖数学家围绕这两个方程争论不休，Clay 数学研究所还把纳维-斯托克斯的存在性与光滑性问题列入千禧年难题。

OpenAI 这个仓库并没有宣称解决了那个千禧问题。它做的是把已知的一些关键步骤，用 Lean 这种交互式定理证明器，一行一行写成机器能核对的证书。换句话说，它不抢功劳，只负责“验货”。

对数学研究者来说，这是把“审稿权”部分交给机器；对AI行业来说，这是少有的、能让外行看一眼就知道AI在硬科学里到底能干什么的样本。

怎么做更省力

把数学结论搬进 Lean，不是把论文复制粘贴，而是要重新写。每一处符号、每一个引用、每一步推导，都要在 Lean 的语法里重新组织，由编译器逐行确认。这件事极其费人，所以仓库里通常会配合使用自动化工具，比如 LLM 辅助把自然语言证明草稿翻译成 Lean 代码，再由人来核对边界条件。

对想理解这类工作的人，与其追仓库里的 Lean 源码，不如先看它附带的“对应论文”：哪些定理被形式化了，证明策略拆成了几步，依赖了哪些已知引理。仓库里通常有一个 README 或 docs 目录会列出来，这是最低门槛的入口。

表格里没有写“读完论文”那行，是因为对非专业读者，论文本身性价比太低，先看仓库自己交代了什么，更省力。

哪些坑要避开

第一，别把它当成“AI证明千禧难题”的信号。仓库标题里有“certificates”，意思是它只负责签发证书，不等于它解决了未解问题。媒体转述时常省略这三个字，读者容易高估。

第二，别低估形式化的人力成本。一段看似十几行的 Lean 代码，可能对应论文里一页纸的推导，反过来也一样。把它当成“全自动写作”的演示，会误判整个领域的进展速度。

第三，stars 数不等于影响力。783 颗星一周内拿到，更多是话题叠加：OpenAI 的名字、流体力学的招牌、形式化社区的稀缺关注，三者叠加放大了传播。它对真正的研究节奏影响有限。

现在就能动手

如果你是技术背景，想顺着这条线走，最直接的下一步是打开仓库的 README，确认 Lean 版本和依赖，装好工具链后跑一遍它自带的测试。如果跑通，至少说明这份证书在当前工具链下是自洽的。

如果你是非技术背景，更实际的做法是把这个仓库当成“看AI怎么参与硬科学”的样本：去看它形式化了什么、没形式化什么、哪些环节仍然要人来兜底。比起读一篇泛泛而谈的综述，这种带着具体代码和论文锚点的仓库，能让你自己得出判断，而不是被任何一方叙述带着走。

边界要清楚：这个仓库不会让你的产品变快，也不会让模型更会“思考”。它改变的是数学结论被信任的方式，这件事重要，但不紧急；知道它存在，比急着使用它更有价值。