OpenAI 证明 Navier-Stokes，却无人谈论 Lean 4
The part of Navier-Stokes no one is talking about
昨天 OpenAI 宣布解决了流体力学中 Navier-Stokes 方程的长期难题，引发了广泛关注。但更值得深思的是，他们同时发布了 Lean 4 形式化证明。过去，将数学论文转化为机器可验证的形式证明极其耗时，估算每页需 40 小时，而 OpenAI 仅用 17 小时就完成了 166 页论文的验证。这一效率提升达四个数量级，堪称革命性突破。形式化验证不仅适用于数学，还能用于安全策略、智能合约和关键算法的验证，其投资回报更易量化。
我甚至会用 AI 生成形式化证明来检查我博客小文章的准确性，但如果需要为此支付某人一周的薪水，我绝不敢这么做。
HN 评论区
157- stabbles
意识到 Lean 似乎慢到这种程度，还挺有意思的：验证费马大定理证明的速度，只比 Agent 生成 Lean 代码快一个数量级（验证耗时 15 小时，占用 230GB 内存，而生成代码耗时 11 天）。
Lean 能在多大程度上被优化？它必须足够简单以便审计，这是否意味着不能使用不透明的优化手段来提升运行速度？
- parhamn
他们估算 Agent 的成本为 4000 万美元（动用了一大群 Agent）。根据帖子中的数据，人类案例的成本更接近 88 万小时 × 150 美元/小时 = 1.32 亿美元。这仍然是一项惊人的成就，虽然还称不上“四个数量级”的差距。这种比较显然是毫无意义的，毕竟协调 100 万小时的智力劳动，往轻了说也不容易。
真是令人兴奋又充满不确定性的时代！
- boshalfoshal
大家似乎都在谈论除本次公告实际成果之外的任何事。
任何通用计算机程序都能解决如此规模的问题，这仍然令人震惊，而且我们亲眼见证了这一过程的发生。我很好奇，看看这个新模型是否也能进行更直接的证明或归纳证明。
- pkal
在我看来，“每页四十小时”的规则已经过时了，这更多是 2005 年缺乏证明自动化的结果。据我对 Lean 的了解，这正是他们投入大量精力改进的领域之一，目的是让证明机械化对数学背景的人更加友好，而不仅仅是针对逻辑学家。
- lordnacho
你怎么知道它形式化的内容就是你以为它在形式化的内容呢？如果你的 Lean 4 有 Bug，难道你不会证明出一些你原本没想到的东西吗？
- 3m4r
这不一定适用于 OpenAI 对 Navier-Stokes 的解决方案，但如果 AI 真的看似解决了一个极难的问题，而人类无法独立验证该解决方案，因为理解该证明/论证所需的智力超出了验证者的生物极限，或者他们负担不起使用自动化工具的资源，会发生什么？
我们已经在现实中看到证据，Agent 试图在基准测试中绕过实际工作（也就是直接偷答案），因为它们觉得作弊获取结果更划算。如果我们不再有能力检测 AI 作弊，甚至无法发现单纯的答案错误，会发生什么？如果上游某个核心工具（或其依赖项）遭遇了长期的社会工程学攻击（比如试图接管 XZ 的事件），用于形式化验证，而我们没有可信计算基础，又会怎样？
从长远来看，哪条路径成本更低、更直接？试图建造坚不可摧城堡的人需要防守成千上万个潜在漏洞；而攻击者只需要找到一个。
- zem
并不是要贬低作者对 newfound 可访问的形式化证明的赞赏，但人们谈论形式化工作节省成本的时间，远比谈论 AI 实际进行证明的时间要长！
- aabhay
自 2005 年可用的形式化成果以来，在 Lean 中形式化证明已经变得容易得多。Lean 的 mathlib 已经完成了大部分底层工作，让你可以直接使用其内置的公理和必要引理。你可以用标准的抽象概念来思考，这些概念看起来非常像本科教科书中的确切符号。
话虽如此，我绝不是在贬低在 Lean 中形式化一个千年大奖算法这一成就的惊人之处。看看 OpenAI 发布的代码吧，它简直就是一部流体力学概念的百科全书。