『ナビア・ストークス方程式の翻訳が失われた理由：LeanによるAIオートフォーマライズの検証は正しい自然言語証明を保証しない』と題されたこの論文は、自然言語の数学的議論をLeanなどの形式証明言語に翻訳するためのAIの使用を検討している。論文では、翻訳後に形式証明は機械的に検証可能であるものの、それが元の自然言語議論への確証を提供するか疑問を呈している。著者らは、OpenAIが発表したナビエ・ストークス方程式の解のblow-upに関する証明を、AIオートフォーマライズの顕著な例として取り上げ、形式化されたLean証明が自然言語のblow-up証明と対応していないことを示している。

著者らは、核心的な困難は自然言語の数学的テキストに固有の曖昧さを解決することにあると主張している。この問題はSolvability Complexity Index（SCI）階層において任意に高い位置にあり、ハルト問題（SCIが1）を含むあらゆる計算問題よりも難しいことを示している。したがって、自然言語からLeanなどの形式言語への意味論的に忠実な翻訳を作成することは、原理的にはあらゆるアルゴリズム問題を解くよりも困難であり、これにより、すべての数学的テキストに対して忠実な翻訳を保証する一般的な方法は存在しないことを意味している。

これを示すために、論文は自然言語の記述や証明をLeanに翻訳する際のAIの誤訳のいくつかの例を示し、自然言語証明とそのLean検証の間に不一致が生じることを示している。OpenAIのナビエ・ストークス証明の場合、形式化されたLean証明は自然言語のblow-up証明と対応していない。これは、Lean証明がそれ自身では正しい可能性があるとしても、AIが形式化すべきだった元の自然言語議論を正確に表していないことを意味し、その結果、Lean検証が元のNL証明の正しさに対する信頼を提供するということが損なわれる。