OpenAI Navier-Stokes发布含Lean 4形式化证明

昨天，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 生成形式化证明来检查我博客文章中的工作。如果必须付给某人一周的工资来检查我的工作，我做梦都不会想到这么做。

形式化验证并不只应用于数学领域。例如，你可以形式化验证一组安全策略是否内部一致，以及在某些假设下它们是否达到了预期目的。你可以形式化验证一份智能合约是否施加了某种最大责任上限。你可以验证关键任务算法的正确性。这些问题比形式化数学研究容易得多，而且回报也更容易量化。

自动化与验证

形式化方法让你得以探索边角地带

什么时候形式化方法才值得投入？