AI说解了千禧难题，怎么先验一遍货

作为一个不懂该数学领域、但有工程验证习惯的人，我试了一下把 OpenAI 关于 Navier-Stokes 千禧年问题的说法拆开验一遍。结论先放这儿，这套方法有用，能帮你不被标题牵着走。Navier-Stokes 是描述水流、空气流这类运动的方程，千禧难题是数学界悬赏的高难问题，据说奖金一百万美元。这次新闻说 OpenAI 内部模型找到了一个解，还给了 165 页证明和 Lean 形式化材料。

公开报道常提到两个数字，一万个智能体跑了 88 小时。这些数字说明投入不小，但不等于证明已经被数学界接受。

我的习惯是看了参数表再下判断。这两个月接触机器人和工程效率工具时，我会问关节的扭矩密度是多少；看 AI 突破时，也要问可复现密度。下面这个流程，大概二十分钟能跑完第一轮。

先建一张核查表。打开浏览器，搜 OpenAI 官方发布页，别从论坛截图找。新建一个文本文件，输三列，说法、证据、缺口。把已解决、165 页证明、Lean 形式化分别抄进去，看到一张三列表。预期结果是你至少能标出两个待查，比如是否公开可下载、模型是否公开。

接着分清两个概念。Lean 是一个证明助手，像给数学证明做自动拼写检查，但它检查的是逻辑步骤。形式化证明是把人写的证明翻译成机器能一行一行读的代码。你不需要懂该数学领域，只需要知道，如果 Lean 检查通过，说明机器认可这段逻辑链条；如果检查失败，先怀疑环境和文件，不立刻怀疑人类。

准备工具时，在电脑浏览器搜 Lean 4 官网，进下载页，点 Download。安装时一路默认。装完打开 VS Code（代码编辑器）。点左侧扩展图标，在搜索框输入 Lean，选择官方插件，点 Install。看到插件页出现 Enabled。预期结果是 VS Code 能识别 `.lean` 文件。

如果你能拿到官方证明包，解压到一个没有中文和空格的文件夹。VS Code 点 `File`，再点 `Open Folder`，选中这个文件夹。等待右下角出现 Lean 启动状态。若没有自动开始，按 `Ctrl+Shift+P`，输入 `Lean: Restart Server`。看到窗口下方出现进度条，文件里可能闪黄色波浪线。预期结果是等几分钟到几十分钟，红色错误变少，最终出现绿色对勾或 `no errors`。如果找不到下载包，就停在第一步，这本身就是缺口。

读结果时别读反了。绿色对勾表示当前文件在当前环境里通过检查。红色波浪线不一定表示 OpenAI 错了，可能是你少装依赖、版本不匹配、文件太大没跑完。踩坑就在这里，常见误判是把 `unknown identifier` 当成证明造假，其实多半是库没装全。解决方式是回到官方包说明，看有没有 `lake update` 或依赖安装步骤。另一个坑是电脑内存不够，大文件卡住。我这边测下来，先开任务管理器看内存占用，超过八成先关浏览器。

最后看争议。在搜索结果里加 `Navier-Stokes controversy` 或 `credit`，你会看到另一种说法，有外部数学家的未发表工作可能被参考，功劳归属有争议。

有数学家在社交平台上提醒，这件事的戏剧性还没结束。

这时候你的核查表第三列该填，需要独立同行评审。

这套流程不保证你懂该数学领域，但能保证你不把公司发布当成学界共识。像产线爬坡数据，一次样机跑通不算量产。下一步可以先找一个几页纸的 Lean 小证明练手，跑通后再碰大文件。

---

📌 本文编译自 Hacker News，原文 https://www.newscientist.com/article/2588063-openai-has-solved-the-navier-stokes-millennium-problem-using-15m-of-ai-effort/

版权归原作者所有，本文为基于公开报道的编译与独立分析。