学者质疑OpenAI数学证明：机检代码与文本推导存在差异

数学界在核验 OpenAI 发布的批量 AI 数学证明时提出了疑虑。剑桥大学研究团队发现，OpenAI 此前公开的纳维-斯托克斯方程证明中，供人类阅读的论文文本与供计算机核验的代码版本并不一致。

OpenAI 在 10 月 6 日集中公开了 722 篇手稿，涵盖针对长期未解数学难题的 372 组研究成果。这些内容均由一个未公开的内部模型生成，平均每个解答耗费约 3 小时计算时间。在此之前数周，OpenAI 曾声称攻克了千禧年大奖难题之一的纳维-斯托克斯方程，并表示新一批成果在另外 3 个千禧年问题上取得了进展，但尚未完全破解。

Lean 形式化代码出现分歧

OpenAI 发布的纳维-斯托克斯证明包含两种形式：一种是由英语和数学符号书写的“自然语言”版本；另一种使用编程语言 Lean 编写，便于计算机逐行核验逻辑步骤。

剑桥大学安德斯·汉森（Anders Hansen）团队发现，两个版本在引理 8.6（Lemma 8.6）处出现偏差。自然语言论文要求某个数值必须低于 m + 4，而 Lean 版本仅要求该数值低于 m + 5，这一条件明显更弱。

研究团队并未断定任何一个版本存在错误。他们担心的是，当 AI 智能体将推导逻辑翻译为 Lean 代码且遇到编译失败时，可能会自行修改论证条件以绕过错误。汉森团队耗时约两周发现了这一分歧，而 OpenAI 声称其模型生成相关证明仅耗费了 88 小时。

汉森指出，大语言模型生成的所有证明仍需要人类学者逐一通读，这给数学界带来了巨大的额外核验负担。

学界对可靠性与归属产生分歧

OpenAI 在回应中表示，公司已知晓两版本的差异，并认为这并未导致证明失效。OpenAI 承诺将在发现错误后修正自然语言文本，并继续对其余论文进行形式化验证。目前仅有部分论文附带 Lean 代码，且这些代码本身尚未经过人工审查。

伦敦帝国理工学院数学家凯文·巴扎德（Kevin Buzzard）表示：“我相信纳维-斯托克斯问题已被正确解决，但我远不确信 PDF 文本中所描述的证明是否完全正确。”

批量 AI 论文的发布在数学界引发了激烈讨论。多伦多大学丹·利特（Dan Litt）认为这是数学领域的重大进展，但也警示盲目宣称“AI 解决了数学”可能会削弱外界对人类数学研究的支持。纽约大学特里斯坦·巴克马斯特（Tristan Buckmaster）则质疑 OpenAI 是否做足尽职调查，以确保模型没有在未经授权的情况下套用人类学者尚未发表的成果。

著名数学家陶哲轩（Terence Tao）在社交平台上表示，这批成果的发布标志着“数学 1.0”的终结。他呼吁行业迈向新时代，“弱化原始解题能力的中心地位，更全面地评估数学研究的整体推进价值”。