纳维-斯托克斯方程证明中没人谈论的部分

昨天，OpenAI 宣布了一项证明，解决了流体动力学中关于纳维-斯托克斯方程的一个长期悬而未决的问题。不出所料，这一宣布引起了广泛关注。但 OpenAI 的工作中有一个方面我还没见任何人提及：他们在发布传统的人类可读证明的同时，还发布了一份 Lean 4 形式化证明。

最近，还有其他不少数学猜想借助 AI 得到了解决，这些成果也都附带了形式化证明，尤其是使用了 Lean 4。

直到不久前，生成机器可验证的形式化证明还是一件极其繁琐的事。2005 年，Henk Barendregt 和 Freek Wiedijk 写道：

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

这就是经验法则：每页四十小时。而且这还是针对本科教材的情况。研究论文比教材密集得多。此外，教材的第 100 页大概主要依赖第 1 到第 99 页的内容。而研究文章中的一句话可能引用之前发表过的任何内容。

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

我本人就曾用 AI 生成形式化证明，只为检查一篇小博客文章。如果必须付给别人一周的工资来检查我的工作，我连想都不敢想。

形式化验证并不仅限于数学。例如，你可以形式化验证一组安全策略是否一致，并验证在给定某些假设的情况下，它们能否达到目的。你可以形式化验证一份智能合约是否设定了某种最大责任限额。你可以验证关键任务算法的正确性。这些问题比形式化数学研究更容易，而且投资回报也更容易量化。