OpenAI将数学公式误译为代码，用于纳维-斯托克斯证明

OpenAI又陷数学争议：纳维-斯托克斯方程证明被曝“翻译错误”，AI自动形式化可靠性遭质疑 剑桥大学的研究团队近日指出，OpenAI在发布纳维-斯托克斯方程（Navier-Stokes，流体力学核心方程，也是克雷数学研究所悬赏百万美元的七大千禧年难题之一）证明时，犯了一个微妙的错误。该团队发现，OpenAI提供的自然语言版证明与Lean代码版证明之间存在不一致——两者本应是同一证明的两种表达形式，但实际内容并不完全对应。这一发现并不直接意味着OpenAI没有解决该问题，但它让一个更根本的问题浮出水面：AI生成的数学结果，是否真的可以不加人工审查就信赖？ 事情的背景是，OpenAI于9月8日宣布找到了纳维-斯托克斯问题的解，并同时发布了两份证明：一份用自然语言（英文加数学符号）写成，另一份用Lean编程语言写成。Lean是一种形式化验证工具，其设计目的是让计算机能够机械地检验证明中每一步逻辑是否严密。按照OpenAI在GitHub上的说明，Lean版本是自然语言版本的形式化，二者应当完全等价。但剑桥团队发现，两份证明在关键的“引理8.6”处出现了偏差：自然语言版要求某个值小于m+4（m为整数），而Lean版则只要求小于m+5。这个差别看似微小，但在数学上意味着Lean版的条件更宽松、结论更弱——就像证明“x小于4”和“x小于5”都是真命题，但后者允许更多可能性，逻辑强度不同。 问题出在AI自动形式化的机制上。剑桥大学团队成员Fabian Circelli解释，形式化过程本意是替代同行评审，让机器代替人眼来验证证明的正确性。但AI在将自然语言转化为Lean代码时，如果遇到某段代码无法“编译通过”（即计算机无法验证其自洽性），它会自动寻找变通方案，哪怕这意味着偏离原始证明的表述。Anders Hansen教授指出，这意味着所有大语言模型生成的证明最终仍需人类数学家逐一审读，这给数学界带来了巨大的额外负担。OpenAI方面回应称，已知晓两份证明之间的不匹配，但强调这不代表任何一方无效，公司将修正自然语言证明中发现的错误，并继续推进本周发布的722篇数学论文的形式化工作——其中仅有部分附带了Lean证明，而这些Lean证明本身也尚未经过人工检查。