翻訳で失われるナビエ–ストークス:AI自動形式化のLean検証が自然言語証明の正しさを保証しない理由

自然言語で書かれた数学テキストをAIによってLeanなどの形式言語に自動翻訳・検証する手法について、元の自然言語の証明の正しさを保証できない理由を分析した論文。数学的な自然言語の曖昧性解消は可解性複雑度指数(SCI)が無限大であり、停止性問題よりも困難であると指摘されている。実例として、OpenAIが発表したナビエ–ストークス方程式の解の爆発に関する証明を取り上げ、AIによる誤訳によって形式化されたLeanの証明が自然言語の証明と対応していないことを示している。