昨天，OpenAI宣布了一项证明，解决了流体动力学中关于Navier-Stokes方程的一个长期悬而未决的问题。这一消息如预期般引发了广泛热议。但OpenAI这项工作中有一个方面，我还没看到任何人谈起：他们在发布传统的人类可读证明的同时，还发布了一份Lean 4形式化证明。
最近已有相当多的数学猜想借助AI得到解决，这些成果同样附带形式化证明，尤其是使用Lean 4完成的形式化证明。
直到不久之前，生成机器可验证的形式化证明仍然极其繁琐。2005年，Henk Barendregt和Freek Wiedijk曾写道：
为了说明形式化所需的工作量，我们估计，将一本本科数学教材中的一页内容形式化，大约需要一个工作周（每天八小时、共五天）。
这就是经验法则：每页四十小时。而且这还是针对本科教材的情形。研究论文的密度远高于教材。此外，教材第100页的内容很可能主要依赖第1到99页的内容，而研究文章中的一句话却可以引用任何已有的成果。假设一篇研究论文的形式化工作量是本科教材一页的20倍，那么将OpenAI那篇166页的论文形式化将需要132,800个工时。而OpenAI只用了17个小时就在Lean中验证了他们的证明。我不太敢用“革命性”这个词，但把任何东西的成本降低四个数量级，就是革命性的。
我曾用AI生成形式化证明来检查自己为一篇小小的博客文章所做的工作。如果每次检查都要付出别人一周的薪水，我是绝不会这么做的。
形式化验证并不仅限于数学。例如，你可以形式化验证一组安全策略是相互一致的，并且在给定某些假设的条件下能够实现其目标。你可以形式化验证一个智能合约设定了某种最大责任上限。你可以验证关键任务算法的正确性。这些问题比形式化数学研究更容易，而且更容易量化投资回报。