昨天，开放人工智能（OpenAI）宣布了一项证明，解决了流体力学中纳维-斯托克斯（Navier-Stokes）方程的一个长期问题。少有人谈的是，他们在发布人类可读证明时，也给出了 Lean 4 形式化证明。近来多个数学猜想被 AI 解决，常附形式化证明。生成机器可验证的证明仍极其繁琐。2005 年，亨克·巴伦德雷赫特（Henk Barendregt）和弗里克·维迪克（Freek Wiedijk）估计，形式化一页本科数学教材约需一个工作周，即四十小时。
正文
昨天 OpenAI 宣布了一项证明，解决了流体力学中纳维-斯托克斯方程的一个长期悬而未决的问题。消息引发大量关注，这在意料之中。但有一点我还没见人谈过：他们在发布普通人可读的证明的同时，还发布了一份 Lean 4 形式化证明。
最近有不少数学猜想被 AI 解决，这些也都附带了形式化证明，用的尤其是 Lean 4。
直到不久之前，生成机器可验证的形式化证明还是极其繁琐的工作。2005 年，Henk Barendregt 和 Freek Wiedijk 写道：
为了说明形式化需要多少工作量，我们估计，把本科数学教材的一页形式化，大约需要一个工作周（五个工作日，每天八小时）。
这就是当时的经验法则：每页四十小时。而且这还是在本科教材的语境下。研究论文比教材密得多。此外，教材的第 100 页多半主要依赖第 1 到 99 页的内容；而研究论文里的一句话，可能引用此前发表过的任何东西。
假设研究论文的形式化难度是本科教材一页的 20 倍，那么把 OpenAI 那篇 166 页的论文形式化，需要 132,800 个人时。而 OpenAI 用 Lean 验证他们的证明只花了 17 小时。我不太想用「革命性」这个词，但把任何事情的成本降低四个数量级，就是革命性的。
我曾用 AI 生成形式化证明来检查自己的工作，不过是为了写一篇小博客文章。如果要花一个人一周的薪水来检查我的工作，我做梦都不会这么做。
形式化验证不只适用于数学。比如，你可以形式化验证一组安全策略是否一致，以及在特定假设下它们能否达成目的。你可以形式化验证一份智能合约设定了某种责任上限。你可以验证关键任务算法的正确性。这些问题比形式化数学研究容易，投资回报也更容易量化。
相关文章
评论
社区在惊叹通用程序实时解决重大数学问题的同时，分歧主轴在于自动形式化是否是老生常谈，以及人类等效成本估算是否靠谱，并浮现对验证可靠性的深层担忧。
认为自动形式化并非新话题，无需反复讨论
- 多个参与者指出，早在本次AI证明之前，数学家就已长期探讨形式化节省人力，且此前AI数学进展时社区已默认使用相关工具，因此不再当作新闻热议（较多人） > 这已不是新闻，此前AI数学进展时大家就默认用了Lean（@hatthew）
认为社区忽视了实际成果与适用性
- 少数意见认为讨论偏题，鲜少触及真实结果或物理应用，强调通用程序解千禧级问题本身令人震惊，而流体方程爆炸解有无现实后果存疑（少数人） > 几乎没人讨论这次宣布里的实际结果，但通用程序能实时解决此等问题仍令人震惊（@boshalfoshal）
质疑人类等效成本估算的准确性
- 根据帖子数字重算，人类工时成本约1.32亿美元而非“四个数量级”差异；另有质疑每页四十小时规则过时，十三万余人时估算离谱，若真实则无人能写教材（少数人） > 按帖子数字人类需约1.32亿美金成本，虽成就惊人但绝非“四个数量级”之差（@parhamn）
指出 Lean 形式化已大幅改善但仍有限制
- 不少评论称Lean及配套库让证明机械化更接近常规数学语言，较早年间容易许多，但基础覆盖不足且仍需学习成本（较多人） > Lean的mathlib已完成底层工作，现在能用类似本科教材的记号思考（@aabhay）
担忧验证速度、工具可靠性与AI不可验证性
- 多方顾虑形式化工具自身可能有漏洞导致证非所想，自动形式化可能含错；另有指出验证速度有限，且若AI解难题而人类无法验证或遭上游攻击，防御将极度困难（较多人） > 若形式化工具自身有缺陷，证出的可能是别的东西（@lordnacho）
有价值的补充
- 有评论呼吁用类似技术理清abc猜想，该问题因几乎无人懂的证明陷入社会建构式悬置（@kens）
- 观察者指出高管称仅花一周即兴尝试即获突破，凸显进展速度反直觉（@khazhoux）
- 也有人注意到学界对独特能力被机械替代的疲惫感将在短期加剧（@AndrewKemendo）