OpenAI 新闻
OpenAI 公布纳维-斯托克斯千禧年难题解法与 Lean 形式化证明
原标题:On the Navier–Stokes Millennium Prize Problem
论文92
我们在此分享一份由 AI 生成的纳维-斯托克斯千禧年大奖难题的解法，包括一份书面报告以及在 Lean 中的形式化证明。
为什么值得读
若证明通过学界核验，将是首个由 AI 攻克并形式化验证的千禧年数学难题，直接检验机器高阶推理的真实边界。
标签
OpenAILeanNavier-Stokes形式化证明数学推理AI4Math