OpenAI的Navier-Stokes发布包含了Lean 4的形式化证明

# 无人谈论的纳维-斯托克斯方程部分 来源：https://www.johndcook.com/blog/2026/09/09/formal-method-revolution/ 昨日OpenAI宣布了一项证明，解决了流体力学中纳维-斯托克斯方程的一个长期悬而未决的问题。此次公告如预期般引发广泛关注，但我注意到OpenAI这项工作中有一个被忽略的维度：他们在发布人类可读证明的同时，也公开了对应的Lean 4形式化证明。 近期已有不少数学猜想通过AI方法得以解决，这些成果同样伴随着形式化证明的发表，尤其多采用Lean 4系统。 直到最近，生成机器可验证的形式化证明仍是一项**异常繁琐**的工作。2005年，Henk Barendregt与Freek Wiedijk曾写道（https://www.cs.ru.nl/~freek/notes/RSpaper.pdf）： > 为说明形式化所需的工作量，我们估算形式化本科数学教材单页内容大约需要一周工作日（五个每天八小时的工作日）。 这曾是经验法则：**每页耗时四十小时**。而这是针对本科教材的估算。研究论文的内容密度远高于教材，且教材第100页的内容通常建立在前99页的基础之上，而研究论文中的单句话语可能涉及所有已发表的先期成果。 假设形式化研究论文的单页工作量是本科教材的20倍，那么形式化OpenAI这篇166页的论文将需要132,800人时。而OpenAI仅用17小时就在Lean中完成了证明验证。我谨慎使用"革命性"一词，但将成本降低**四个数量级**确实具有颠覆意义。 我曾为撰写一篇简短的博客文章，使用AI生成形式化证明来检验工作。若需支付他人一周薪资来验证成果，我根本不敢想象这种做法。 形式化验证不仅适用于数学领域。例如，可以形式化验证安全策略集的内在一致性，并确认在特定假设下能实现预期目标；可以验证智能合约是否确实设定了最高责任限额；还能验证关键任务算法的正确性。这些问题的形式化难度低于数学研究，且投资回报率更易量化。 ## 相关文章 - 自动化与验证（https://www.johndcook.com/blog/2025/12/24/automation-and-validation/） - 形式化方法助你探索边界（https://www.johndcook.com/blog/2016/07/11/formal-methods-let-you-explore-the-corners/） - 形式化方法何时值得投入？（https://www.johndcook.com/blog/2020/12/03/formal-proof-roi/）