arXiv 论文指出 AI 自动形式化验证存在语义失真：涵盖 OpenAI 纳维-斯托克斯方程案例

论文指出 AI 自动形式化验证因自然语言翻译到形式语言（如 Lean）难以保证语义保真，可能无法为原始数学论证提供可信度。研究表明消除数学自然语言歧义的理论复杂度在可解度复杂度指标（SCI）层级中为无穷大，难度高于停机问题；文中给出了包括 OpenAI 纳维-斯托克斯方程解爆破证明在内的多个错误翻译案例，表明其 Lean 形式化证明与自然语言证明并不对应。