OpenAI的Navier-Stokes版本包含Lean 4正式证明

昨天，OpenAI宣布了一项证据，解决了关于流体动力学中纳维尔-斯托克斯方程的长期问题。正如人们所预料的那样，这一消息引起了广泛关注。但OpenAI的工作有一个方面是我没有见过任何人谈论的：他们在发布传统的人类可读证明的同时发布了Lean 4正式证明。

最近使用人工智能解决了许多其他数学猜想，这些猜想也伴随着正式证明，特别是使用Lean 4。直到最近，生成机器可验证的形式证明一直是极其乏味的。

2005年，Henk Barendregt和Freek Wiedijk写道为了表明正式化需要多少工作，我们估计大约需要一个工作周（五个工作日，八个工作小时）才能正式化本科数学教科书的一页。这是经验法则：每页四十小时。

这是在本科课本的背景下。研究出版物比教科书密集得多。此外，教科书的第100页可能主要取决于第1页到第99页的材料。研究文章中的一句话可以引用以前发表过的任何东西。比如说一篇研究文章需要比本科课本上的一页多花20倍的精力来形式化。

然后，将OpenAI的166页论文正式化将需要132，800个工时。OpenAI花了17个小时来验证他们在精益中的证明。

我不愿意使用“革命性”这个词，但将任何东西的成本降低四个数量级都是革命性的。我使用人工智能生成正式证据来检查我的工作，只是为了一篇小博客文章。如果我必须支付某人一周的工资来检查我的工作，我做梦也不会这么做。

形式验证不仅仅适用于数学。例如，您可以正式验证一组安全策略是否一致，并且在给定某些假设的情况下，它们是否能够实现其目的。您可以正式验证智能合同是否施加了一定的最高责任。您可以验证关键任务算法的正确性。

这些问题比正式化数学研究更容易，而且更容易量化投资回报。相关员额