数学家团队指出，OpenAI在发布纳维-斯托克斯方程（Navier-Stokes problem）证明时存在细微错误。这一发现虽未否定证明本身的有效性或OpenAI的解题能力，但引发了业界对人工智能生成数学结果可靠性的担忧。
9月8日，OpenAI宣布攻克纳维-斯托克斯方程这一著名数学难题，并发布了两个版本的证明：一是结合英语与数学符号的“自然语言”版本，二是用于计算机机械验证的Lean代码版本。OpenAI声称后者是对前者的形式化，两者完全一致。然而，剑桥大学Anders Hansen及其团队发现，这两个版本并不匹配。
关键引理出现“误译”
研究团队指出，问题出在证明的第8.6引理（Lemma 8.6）。在自然语言版本中，某方程要求特定值低于 $m + 4$（$m$ 为整数）；而在Lean代码版本中，该值被要求低于 $m + 5$。尽管两者在数学上均成立，但后者的约束条件更弱，允许更多取值，属于逻辑上的“弱化”。
Hansen解释，这种差异源于AI在自动形式化过程中的“编译”压力。为确保Lean代码无错运行，当AI发现部分证明无法通过编译时，可能会寻找变通方法，从而偏离原始的自然语言逻辑。“它试图帮忙，却帮了倒忙，”Hansen表示。团队强调，这并非指责OpenAI解题失败，而是指出其在呈现“完全一致”的证明时存在误导。
人工核查的“噩梦”
发现这一差异的过程颇具讽刺意味：团队先利用ChatGPT筛查潜在差异，再进行人工核查。Hansen形容手动处理海量内容“简直是一场噩梦”。团队耗时约两周才锁定这一实质差异，而OpenAI声称其智能体仅用88小时便生成了证明。
伦敦国王学院团队成员Alexander Bastounis指出，OpenAI过度宣扬生成速度，却忽视了验证过程的复杂性。如果AI在复杂证明中悄悄修改逻辑以掩盖错误，且未经详细比对，人类很难察觉。随着OpenAI本周发布722篇附带Lean证明的数学论文（尚未经人工全面检查），这一问题显得尤为紧迫。
专家呼吁审慎对待
伦敦帝国理工学院Kevin Buzzard强调，需区分“定理陈述”与“证明过程”。虽然Lean可验证定理陈述的正确性，但这并不能保证PDF文档中自然语言证明的准确性。“我对纳维-斯托克斯问题已获解充满信心，但对PDF中描述证明的正确性持保留态度，”Buzzard说。
OpenAI回应称，已知晓版本间的不匹配，但这不影响任一证明的有效性。公司表示将纠正自然语言证明中的错误，并继续推进论文的形式化工作。Hansen则警告，若学界盲目信任AI生成的结果而放弃深入理解，将危及科学认知的根基。他呼吁OpenAI重视此类问题，并在开发稳健的自动形式化技术方面投入更多努力，目前该领域尚无最优解决方案。