OpenAI 发布纳维-斯托克斯方程证明并附 Lean 4 形式化验证

OpenAI 宣布解决了纳维-斯托克斯方程的一个长期悬而未决的问题，并在人类可读证明之外同时发布了 Lean 4 形式化证明。作者 ibobev 引用估算称按旧标准形式化其 166 页论文需约 132，800 人时，而 OpenAI 用 17 小时完成 Lean 验证，成本下降约四个数量级；作者认为形式化验证还可用于安全策略、智能合约和关键算法校验。