OpenAI纳维-斯托克斯证明遭质疑：新研究揭示Lean验证无法保证AI数学证明忠实原意

数学家Alexander Bastounis、Fabian Circelli和Anders C. Hansen在arXiv发表论文，质疑AI自动形式化验证的可靠性，矛头直指OpenAI此前宣布的纳维-斯托克斯方程解爆破证明。自动形式化是指AI系统将自然语言数学证明翻译为Lean等形式化语言，再由机器机械验证其正确性的流程。研究指出该流程存在根本性缺陷：对自然语言数学文本进行语义忠实的歧义消解，在可解性复杂度指数（SCI）层级中处于任意高层级（SCI=∞），这意味着语义忠实的AI自动形式化比包括停机问题在内的任何可计算问题都更难。作者通过多个实际案例展示了AI在将自然语言陈述和证明翻译为Lean时产生的错误，导致自然语言证明与其Lean“验证”之间出现语义不匹配，其中就包括OpenAI宣布的纳维-斯托克斯证明——研究表明其形式化的Lean证明与原自然语言证明并不对应。论文共25页、含4幅图表，横跨偏微分方程分析、人工智能与数理逻辑三个学科，对当前“AI生成数学证明+形式化验证”的技术路线提出了深层次的理论挑战。

事件分析

核心观点：Lean验证只能保证翻译后的逻辑自洽，却无法保证翻译忠实原意——AI数学证明的信任链恰在“翻译”环节断裂。