数学家指出 OpenAI 的 Navier-Stokes 证明在转为 Lean 代码时存在误译

OpenAI mistranslated mathematics into code for its Navier-Stokes proof

数学家团队指出，OpenAI 的 Navier-Stokes 自然语言证明与 Lean 形式化版本存在差异，但这不代表任一版本无效。Lemma 8.6 中，自然语言版本要求某个值小于 m + 4，Lean 版本却要求小于 m + 5，条件更弱；团队借助 ChatGPT 排查并人工核验，约用两周找到这一差异。