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

文章称 OpenAI 在公布 Navier-Stokes 方程证明时同步发布了 Lean 4 形式化证明。作者引用 2005 年 Barendregt 与 Wiedijk 的估算——形式化一页本科数学教材约需一个工作周（40 小时）——并假设研究论文形式化难度为教材的 20 倍，据此推算 166 页论文需约 132,800 人时，而 OpenAI 用 17 小时在 Lean 中完成验证，成本下降约四个数量级。作者认为形式化验证还可用于安全策略一致性、智能合约责任上限和关键算法正确性等更易量化回报的场景。上述成本对比为博客作者的估算与假设，OpenAI 证明的具体细节和验证口径未在输入中提供。

AI推荐理由 文章指出 OpenAI 在发布 Navier-Stokes 方程证明的同时提供了 Lean 4 形式化证明，并引用 2005 年 Barendregt 与 Wiedijk 的估算（每页本科教材约需 40 小时形式化）来对比：按该估算，166 页论文形式化需约 132,800 人时，而 OpenAI 用 17 小时在 Lean 中验证了证明，成本降低约四个数量级。这是输入中具体的新信息，也点出形式化验证可扩展到安全策略一致性、智能合约责任上限、关键算法正确性等场景。局限在于：文章为个人博客的估算与评论，OpenAI 的 Lean 证明细节、验证范围及 17 小时口径均未在输入中给出可核验证据，成本对比基于假设性外推，不能视为已证实的突破。