AI自動形式化はNavier-Stokes証明を保証しない
原題: Navier–Stokes Lost in Translation
なぜ重要か
AI主導の数学証明に対する信頼性の根拠が揺らぐ可能性があり、OpenAIを含む大手企業の形式検証戦略全体に再考を迫る内容だ。
2026年10月6日、ケンブリッジ大学などの研究者Alexander Bastounis、Fabian Circelli、Anders C. Hansenがarxivに論文を投稿。自然言語の数学的証明をLeanへ翻訳するAI自動形式化（autoformalisation）が、元の自然言語証明の正しさを保証しないと主張。OpenAIが発表したNavier-Stokes方程式の解の爆発（blow-up）証明を具体例として挙げ、Lean検証済みの形式証明が元の自然言語証明と対応していないことを示した。
数学証明の自動検証手法として注目を集めるAI自動形式化。この手法では、AIが自然言語（NL）で書かれた数学的テキストをLeanなどの形式言語に翻訳し、機械的に検証する。OpenAIはこの手法を活用してNavier-Stokes方程式の解の爆発に関する証明を発表していた。
今回の論文はその手法の根本的な限界を指摘する。核心となる主張は、自然言語テキストの曖昧性を解消しながら意味的に忠実な翻訳を行う問題が、計算複雑性の枠組みである「Solvability Complexity Index（SCI）階層」において無限大（SCI＝∞）に位置するというものだ。平たく言えば、意味的に忠実な自動形式化を保証することは、停止問題（SCI＝1）よりも難しい。停止問題すら解けないのに、翻訳の完全な正しさを機械的に担保することは原理的に不可能だと論文は述べる。
著者らはこの理論的主張を裏付けるため、実際にAIがNL文とLean翻訳を誤訳した複数の具体例を提示。中でもOpenAIのNavier-Stokes証明について、形式化されたLean証明が元のNL証明における解の爆発（blow-up）の議論と対応していないことを詳細に分析した。
論文は25ページ、4つの図を含む。数学的偏微分方程式（math.AP）、人工知能（cs.AI）、論理学（math.LO）の複数分野にまたがる内容で、Lean検証が「正しい証明の印」として機能するという一般的な信念に疑問を呈している。