# OpenAI 发布纳维-斯托克斯方程证明并附 Lean 4 形式化验证

- 来源：Hacker News 热门（buzzing.cc 中文翻译）
- 作者：ibobev
- 发布时间：2026-09-11 07:01
- AIHOT 分数：79
- AIHOT 标记：已收录
- AIHOT 链接：https://aihot.news/items/cmtw5rln304sjrolkepoca0qv
- 原文链接：https://www.johndcook.com/blog/2026/09/09/formal-method-revolution

## AI 摘要

OpenAI 宣布解决了纳维-斯托克斯方程的一个长期悬而未决的问题，并在人类可读证明之外同时发布了 Lean 4 形式化证明。作者 ibobev 引用估算称按旧标准形式化其 166 页论文需约 132,800 人时，而 OpenAI 用 17 小时完成 Lean 验证，成本下降约四个数量级；作者认为形式化验证还可用于安全策略、智能合约和关键算法校验。

## 正文

昨天，OpenAI 宣布了一项证明，解决了流体力学中关于 Navier-Stokes 方程的一个长期悬而未决的问题。正如人们所预料的那样，这一宣布引发了大量热议。但 OpenAI 这项工作有一个方面我还没见任何人谈及：他们在发布传统的人类可读证明的同时，还发布了一份 Lean 4 形式化证明。

最近，已有相当多的其他数学猜想借助 AI 得到解决，而这些成果同样附带了形式化证明，尤其是使用 Lean 4 完成的。

直到不久之前，生成机器可验证的形式化证明一直是极其繁琐乏味的工作。2005 年，Henk Barendregt 和 Freek Wiedijk 写道

为了说明形式化需要多少工作量，我们估计，将一本本科数学教科书中的一页形式化，大约需要一个工作周（五个工作日，每天八小时）。

这就是经验法则：每页四十小时。而且这还是针对本科教科书而言。研究论文的密度远高于教科书。此外，教科书第 100 页可能主要依赖于第 1 页到第 99 页的内容。而研究论文中的一句话，可能引用此前发表的任何东西。

假设一篇研究论文的形式化工作量是本科教材每页的 20 倍。那么，将 OpenAI 那篇 166 页的论文形式化，就需要 132,800 个工时。而 OpenAI 在 Lean 中验证他们的证明只用了 17 个小时。我犹豫要不要用“革命性”这个词，但把任何事物的成本降低 四个数量级，就是革命性的。

我曾用 AI 生成形式化证明来检查自己的工作，仅仅是为了一篇小博文。如果我要花一个人一周的薪水来请人检查我的工作，我做梦都不会这么做。

形式化验证不仅仅适用于数学。比如说，你可以形式化验证一组安全策略是否一致，以及在特定假设下它们是否能达成其目的。你可以形式化验证一份智能合约是否施加了某个特定的最大责任上限。你可以验证关键任务算法的正确性。这些问题比形式化数学研究更容易，也更容易量化投资回报。