数学家Alexander Bastounis、Fabian Circelli和Anders C. Hansen在arXiv发表论文，质疑AI自动形式化验证的可靠性，矛头直指OpenAI此前宣布的纳维-斯托克斯方程解爆破证明。自动形式化是指AI系统将自然语言数学证明翻译为Lean等形式化语言，再由机器机械验证其正确性的流程。研究指出该流程存在根本性缺陷：对自然语言数学文本进行语义忠实的歧义消解，在可解性复杂度指数（SCI）层级中处于任意高层级（SCI=∞），这意味着语义忠实的AI自动形式化比包括停机问题在内的任何可计算问题都更难。作者通过多个实际案例展示了AI在将自然语言陈述和证明翻译为Lean时产生的错误，导致自然语言证明与其Lean“验证”之间出现语义不匹配，其中就包括OpenAI宣布的纳维-斯托克斯证明——研究表明其形式化的Lean证明与原自然语言证明并不对应。论文共25页、含4幅图表，横跨偏微分方程分析、人工智能与数理逻辑三个学科，对当前“AI生成数学证明+形式化验证”的技术路线提出了深层次的理论挑战。
事件分析
这项研究从可计算性理论层面揭示了自动形式化的理论天花板：SCI层级分析表明，语义忠实的翻译可能超出任何算法的求解能力，意味着机器验证通过的证明与原始论证之间的语义鸿沟无法靠更强的验证器弥合。对AI for Math赛道而言，这一结论直接冲击了“AI生成+形式化验证”的技术叙事，OpenAI等公司发布的重大数学成果可能需要重新审视其验证链条。但研究并未否定形式化方法的价值，而是提示行业重心应从“验证翻译结果”转向“保证翻译质量”，例如发展人机协同审查、多模型交叉翻译校验等机制。后续值得关注的方向包括：OpenAI团队是否会正面回应质疑、是否存在可修复NL与Lean文本对应关系的方案，以及Lean社区是否会建立更严格的自动形式化质量评估标准。
核心观点：Lean验证只能保证翻译后的逻辑自洽，却无法保证翻译忠实原意——AI数学证明的信任链恰在“翻译”环节断裂。
原文链接：Hacker News
