10月6日，OpenAI集中发布722篇由AI生成的数学论文，在学界引发震动。次日，3篇关于霍奇猜想的论文因证明中出现符号错误而被撤回。关于AI数学研究的争议已不止于论文对错，更涉及形式化验证的局限与研究责任归属。本文作者指出，速度与规模无法替代理解、复核和同行交流；数学界对AI论文的审视，也关乎更广泛的AI安全问题。 撰文 | 倪忆 2026 年 10 月 6 日，OpenAI 一口气发布了 722 篇完全由其内部 AI 大模型生成的论文，宣称解决了 377 个数学难题。消息刚一传出，立刻震动数学界，舆论场上更是一片“AI终结数学”的声音。 从数学界的角度看，OpenAI 这一做法问题颇多。限于篇幅，本文只注重于这些论文的检验与理解。 与发布时的高调相反，仅过了一天，OpenAI 就悄悄撤回了三篇关于 Hodge 猜想的论文。原因是某处出现了一个正负号的错误，使得证明完全无效。具有讽刺意味的是，这个符号错误是 Reddit 网友用 OpenAI 的 Astra 模型发现的。OpenAI 自己发布论文之前，没有用 Astra 检查一遍吗？ 这让人不禁想起《伊利亚特》里的名场面：在特洛伊战争最激烈的时刻，奥林匹斯众神纷纷下场参战。战神阿瑞斯自以为于人间全无敌，结果阿尔戈斯国王狄俄墨得斯在雅典娜的帮助下，一标枪刺中阿瑞斯的小腹，让阿瑞斯狼狈逃回奥林匹斯山。 凡人在神的帮助下能击败神，在 AI 的帮助下也能超越 AI。 OpenAI 这一批论文里，只有一篇发布之前经过了人类的验证，不到一半经过了 Lean 的形式化检验。那些没有 Lean 验证的，我认为出错可能性非常高。毕竟 AI 连正负号这样愚蠢的错误都能犯，更不用说那些非常微妙的逻辑错误。 我前段时间读过一篇论文，是人类写的，但是声明用 AI 检验过。我粗略看了一下，没看细节，只看证明框架，就发现两个逻辑漏洞，包括主定理的叙述都有错误。这两个漏洞并非实质性错误，但如果 AI 连这种逻辑漏洞都看不出来，它自己写的论文也可能会有类似甚至更严重的问题。 即便是经过 Lean 形式化检验的论文，也只能说正确的可能性更大，而不是一定正确。 首先，Lean 的系统本身就会有漏洞。两个月前刚刚发生过一件事，有人利用 Lean 的系统漏洞，往 GitHub 上放了一篇主文件只有 20 行代码的错误证明，并由 Lean 编译通过。以现在 AI 的能力，完全有可能发现新的漏洞，并利用这一漏洞来制造能够通过 Lean 形式化检验的错误论文。 其次，需要验证是否忠实地将数学内容翻译成了 Lean 的语言。就在 10 月 6 日当天，预印本网站上出现一篇论文，指出 OpenAI 所宣称的解决千禧年问题 Navier-Stokes 方程论文，其中一个命题的 Lean 形式化跟命题本身的数学内容不一致。这并不说明论文有错，而是说 AI 给出的 Lean 形式化验证有错，但也足以说明 Lean 没有那么靠谱。 然而，很多网络评论对这些论文是否正确并不在意。有人说，OpenAI 722 篇论文只有 3 篇撤回，这个可靠程度在工程上已经非常高了。 这个说法的问题在于，仅仅第二天就有 3 篇撤回，那么时间长了，还会有多少论文被发现错误呢？用工程来打一个比喻，假如有一个超级智能体宣称自己 3 小时就能造一座桥，为了秀肌肉，它一次造了 722 座桥，结果到第二天就垮了 3 座，那你还敢使用其余的桥吗？ 事实上，这几天下来又有多篇论文被研究者发现有错误。 还有评论说，人类也会犯错，就算数学大师写的论文，经过多年后也会发现错误。 正是因为人类也会犯错，所以哪怕是数学大师写的论文，也要经过学术共同体最严格的检验。即便已经发表在杂志上，也不能确保一定就是对的，发现严重错误后还要修正或者撤回。我以前曾介绍过 Joan Birman 的故事。1973年，Birman 和 Hilden 在《数学年刊》上发表了一篇论文，其中包含7个定理。2016年，有两名数学家发现这篇论文中的定理5是错误的。Birman 和 Hilden 检查了 MathSciNet 上引用他们论文的全部42篇文献，确认没有一篇引用了错误的定理5，并在更正中加以说明。他们的更正发表于2017年，距离前一篇论文已经有44年。 人类写的论文，有人类作者为其负责。什么叫负责？就是公布论文前精心打磨，避免错误，尽最大可能把论文写得容易被人读懂；有义务在各种场合解释自己的工作，回答同行们的问题；发现错误了，需要改正。 不管是证明费马大定理的 Wiles，还是证明庞加莱猜想的 Perelman，他们都做过多场学术报告，并用各种方式回答同行们提出的问题，而不是说把论文贴出来就撒手不管。Wiles 原始证明被发现有错误，他花了一年时间跟 Taylor 一起弥补了漏洞。Perelma