OpenAI 纳维-斯托克斯证明：Lean 4 验证仅 17 小时

jedisct1 · x · 2026-09-11

OpenAI 宣布解决流体力学纳维-斯托克斯方程的一个长期悬而未决问题，但少有人注意的是：他们在人类可读证明之外同时发布了 Lean 4 机器可验证的形式化证明。John D. Cook 算了一笔账：按 2005 年的经验法则，形式化一页本科教材约需一周（40 小时），研究论文密度更高，166 页论文按 20 倍难度估计需约 13.28 万人工时——而 OpenAI 用 17 小时完成验证，成本降低约四个数量级。作者认为这堪称革命性：形式化验证从此可用于日常校验数学工作，且不限于数学领域。