OpenAI 发布纳维-斯托克斯证明，同步公开 Lean 4 形式化验证
2026.09.11 · 事件 · AI 事件 · 社区热议
OpenAI 用 17 小时完成 Lean 4 验证，成本降低四个数量级。
OpenAI 昨日宣布解决了纳维-斯托克斯方程的长期问题，并同时发布了传统可读证明和 Lean 4 形式化证明。据原文，形式化验证曾极其繁琐，2005 年估算每页本科教材需一周工作量，而 OpenAI 的 166 页论文仅用 17 小时完成 Lean 验证，成本降低四个数量级。
- OpenAI 发布纳维-斯托克斯证明
- 同步发布 Lean 4 形式化证明
- 验证耗时 17 小时
- 成本降低四个数量级
- 形式化验证可用于安全策略等
为什么值得看
形式化验证成本骤降，或改变数学与软件验证方式。
适合谁关注
关注 AI 数学、形式化验证及软件可靠性的开发者。