OpenAI 纳维-斯托克斯证明靠 Lean 形式化验证

OpenAI 宣布在纳维-斯托克斯方程问题上取得突破，并在人类可读证明之外发布了 Lean 4 机器可验证的形式化证明，验证仅耗时 17 小时。Lance Fortnow 撰文指出，OpenAI 与 Alpöge-Buckmaster 团队的相关公告都重度依赖 Lean 形式化验证，引发学界争论：Lean 是否会成为数学成果发表的新门槛。

2026-09-10 ~ 2026-09-11 · 3 条相关

• OpenAI 与 Alpöge-Buckmaster 攻克 Navier-Stokes 都重度依赖 Lean 形式化验证 — fortnow · 2026-09-10
• OpenAI 与 Navier-Stokes 证明都靠 Lean 验证，学界争论成新门槛？ — CsabaSzepesvari · 2026-09-10
• OpenAI 纳维-斯托克斯证明：Lean 4 验证仅 17 小时 — jedisct1 · 2026-09-11