昨天，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 生成形式化证明来检查自己的工作，仅仅是为了一篇小博文。如果我要花一个人一周的薪水来请人检查我的工作，我做梦都不会这么做。
形式化验证不仅仅适用于数学。比如说，你可以形式化验证一组安全策略是否一致，以及在特定假设下它们是否能达成其目的。你可以形式化验证一份智能合约是否施加了某个特定的最大责任上限。你可以验证关键任务算法的正确性。这些问题比形式化数学研究更容易，也更容易量化投资回报。
Yesterday OpenAI announced a proof that settled a long-standing question about the Navier-Stokes equations from fluid dynamics. The announcement has created a lot of buzz, as one would expect. But there’s an aspect of OpenAI’s work that I haven’t seen anyone talk about: they posted a Lean 4 formal proof at the same time as their conventional human-readable proof.
Quite a few other mathematical conjectures have been settled recently using AI, and these have also been accompanied with formal proofs, using Lean 4 in particular.
Until very recently, generating machine-verifiable formal proofs has been excruciatingly tedious. In 2005, Henk Barendregt and Freek Wiedijk wrote
To give an indication of how much work is needed for formalisation, we estimate that it takes approximately one work-week (five work-days of eight work-hours) to formalise one page from an undergraduate mathematics textbook.
That was the rule of thumb: forty hours per page. And this in the context of undergraduate textbooks. Research publications are much denser than textbooks. Furthermore, page 100 of a textbook probably depends mostly on material on pages 1 through 99. A sentence in a research article could cite anything that has been published before.
Say a research article takes 20 times more effort to formalize than page in an undergraduate textbook. Then formalizing the 166-page paper from OpenAI would take 132,800 person-hours. It took OpenAI 17 hours to verify their proof in Lean. I hesitate to use the word “revolutionary,” but lowering the cost of anything by four orders of magnitude is revolutionary.
I’ve used AI to generate formal proofs to check my work just for a little blog post. I wouldn’t dream of doing that if I had to pay someone a week’s salary to check my work.
Formal verification doesn’t just apply to mathematics. You could, for example, formally verify that a set of security policies are consistent and that, given certain assumptions, they accomplish their purpose. You could formally verify that a smart contract imposes a certain maximum liability. You could verify the correctness of mission-critical algorithms. These problems are easier than formalizing mathematics research, and it is easier to quantify the return on investment.