OpenAI 纳维-斯托克斯 Lean 形式化：约 40 万行代码，编译一次约 20 小时

参与 OpenAI 纳维-斯托克斯方程求解形式化的开发者分享了形式化验证的工程细节，最终仓库约 40 万行 Lean 代码，编译一次约需 20 小时。每次运行都会冒出代码中的小错误，需要逐一修复，这展示了前沿模型数学成果形式化验证的真实工程量。