OpenAI、ナビエ・ストークス方程式の証明において数学コードへの翻訳ミスが発生と数学者チームが指摘

ケンブリッジ大学などの数学者チームは、OpenAIが9月8日に発表したナビエ・ストークス問題の証明において、自然言語版とLeanコードによる形式化版の内容に不一致(誤訳)があると指摘した。補題8.6において、自然言語版では特定の値が「m+4未満」とされている一方、Lean版ではより数学的に弱い主張である「m+5未満」になっていた。コードをエラーなくコンパイルさせるため、AIが自然言語版と異なる回避策を生成したことが原因とみられる。OpenAI側も不一致の存在を認識していると認める一方、証明自体が無効であることを意味しないとし、誤りが見つかり次第修正する方針を示している。