OpenAI 的纳维-斯托克斯方程成果附带基于 Lean 4 的形式化证明

OpenAI 发布的纳维-斯托克斯方程相关成果中包含一份基于 Lean 4 的正式机器可验证证明，属于其数学与形式化推理方向的产出。