OpenAI 纳维-斯托克斯证明：Lean 4 验证仅 17 小时
jedisct1 · x · 2026-09-11
OpenAI 宣布解决流体力学纳维-斯托克斯方程的一个长期悬而未决问题，但少有人注意的是：他们在人类可读证明之外同时发布了 Lean 4 机器可验证的形式化证明。John D. Cook 算了一笔账：按 2005 年的经验法则，形式化一页本科教材约需一周（40 小时），研究论文密度更高，166 页论文按 20 倍难度估计需约 13.28 万人工时——而 OpenAI 用 17 小时完成验证，成本降低约四个数量级。作者认为这堪称革命性：形式化验证从此可用于日常校验数学工作，且不限于数学领域。
所属事件:OpenAI 纳维-斯托克斯证明靠 Lean 形式化验证(3 条相关)→
「漫话AGI」频道最新
- Epoch 数据：中国最强模型平均落后美国 6.3 个月，实际差距近 8 个月 — deanwball · 2026-09-11
- 2029 年开源模型加合成技术或让生物风险「近乎零门槛」 — JMannhart · 2026-09-11
- Gary Marcus 认同：安全是对齐中无法靠基准测试遮羞的部分 — GaryMarcus · 2026-09-11
- 玩家自述：自从有了 AI 生成，打游戏再也提不起劲 — iruletheworldmo · 2026-09-11
- NBER 工作论文 32% 由 AI 生成，经济学家呼吁「人类写作」规范 — paulnovosad · 2026-09-11
- Claude 把黎曼猜想相关界从 41.6% 推到 67.2%，年内或解多个千禧难题 — haider1 · 2026-09-11