ナビエ・ストークス方程式の翻訳ミス：LeanによるAI自動形式化検証が自然言語証明の正しさを保証しない理由

自動形式化は、AIによって生成されたものを含む数学的テキストの検証にますます使用されています。例えば、OpenAIが発表したナビエ・ストークス方程式の解の爆発に関する証明などがこれにあたります。 このプロセスでは、AIシステムが自然言語（NL）からLeanのような形式言語へテキストを翻訳します。 この翻訳が完了すると、形式言語で表現された議論は機械的に検証することが容易になります。 本稿の目的は、このプロセスが元のNL議論に対して信頼性を提供しない可能性がある理由を実証することです。 これは、意味論的に忠実な翻訳を実行する際の様々な困難に起因します。 特に、意味論的に忠実な翻訳を提供するために必要な、数学的NLテキストにおける曖昧性の解消問題は、Solvability Complexity Index（SCI）階層／算術階層において任意に高い位置にあり（SCI = ∞）、計算不可能であることを強調します。 したがって、非公式に言えば、意味論的に忠実なAI自動形式化を提供することは、停止問題（SCI = 1）を含むあらゆる計算問題よりも困難です。 この結果の影響を示すために、NLのステートメントや証明をLeanにAIが誤って翻訳した実例をいくつか提供します。 これにより、NL証明とそのLeanでの「検証」との間に不一致が生じます。 これには、OpenAIが発表したナビエ・ストークス方程式の証明も含まれます。 特に、形式化されたLean証明は、ナビエ・ストークス方程式の解の爆発に関するNL証明に対応していないことを示します。