Alexander Bastounis、Fabian Circelli 和 Anders C. Hansen 於 2026 年 10 月 6 日在 arXiv 發表論文《Navier–Stokes Lost in Translation》，探討利用 AI 將自然語言數學文本自動形式化（Autoformalisation）為 Lean 等形式語言並進行機械驗證的過程。該論文指出，由於在進行語義忠實的翻譯時面臨巨大困難，此過程可能無法對原始自然語言論證提供信心。作者特別強調，解決數學自然語言文本中的歧義問題，在可解性複雜度指數（SCI）層級或算術層級中處於任意高的位置（SCI = ∞）。這意味著，提供語義忠實的 AI 自動形式化比任何計算問題（包括 SCI = 1 的停機問題）都更困難。為了展示這一結果的影響，論文提供了多個 AI 將自然語言陳述和證明誤譯為 Lean 的實際例子，導致自然語言證明與其 Lean「驗證」之間出現不匹配。這些例子包括 OpenAI 先前宣布的納維-斯托克斯方程解的爆破（blow-up）證明。論文特別指出，形式化的 Lean 證明並不對應於納維-斯托克斯方程解的爆破的自然語言證明。
事件背景
自動形式化（Autoformalisation）是指將自然語言（NL）翻譯為 Lean 等形式語言的過程，一旦翻譯完成，形式語言中的論證即可輕鬆進行機械驗證。此方法 increasingly 被用於驗證數學文本，包括由 AI 生成的文本，例如 OpenAI 宣布的納維-斯托克斯方程解的爆破證明。可解性複雜度指數（SCI）層級用於對計算問題的難度進行分類，其中停機問題位於 SCI = 1 級別。
社群觀察
社群討論中，用戶 j2kun 認為這突顯了至少在同行評審完成之前，AI 生成的證明應被描述為解決問題的「主張」，並指出認為 AI 公司超越同行評審的觀點是有害的。用戶 ComplexSystems 指出，該論文的核心主張似乎是 OpenAI 並未真正證明納維-斯托克斯問題，因為 LLM 未能正確形式化原始的「自然語言」想法。用戶 buzzy_hacker 詢問這是否僅質疑自然語言證明與 Lean 證明之間的等價性，而非 Lean 證明本身的正確性。用戶 sigbottle 則探討了意義危機理論的可能性，並指出即使證明可能有誤，檢查問題陳述通常比檢查解決方案更容易。
