数学输出究竟是什么？AI 生成证明与数学理解之争

距离那个包含 700 多份文档以及（远少于这个数量的）AI 生成证明的 Lean 形式化的 GitHub 仓库被公开，已经过去将近一周了，但感觉上要长得多。我自己对 AI 的使用持复杂态度。我在日常工作中使用它，我们会把正在实现、且永远不会公开的东西形式化（以前用 Isabelle，现在用 Lean）。我也曾用 AI 来填补我对正在撰写的研究论文背景材料的理解，尝试寻找难以找到的参考文献，以及生成一些用我不熟悉的专业语言进行计算的代码。我还用它来翻译和从旧扫描文档中提取材料。但我不愿仅仅让它去证明我想知道的东西。几年前我这么做过，当时这些系统还很不稳定，最终我只好从头手工推导出我从它那里得到的结果，因为我丢失了对话记录，而且我无论如何都需要一个证明。我选择不让它为我起草或撰写论文，因为我觉得那实在让人难以忍受。

我花了也许比应该花的更多的时间，试图衡量人们的看法；当时我不想发表评论。有些人显然非常有兴趣从这 700 多份文档中挖掘洞见，或者拿过来改进结果（例如乘法算法复杂度上界一直在快速下降，但这些可能大多只是在 X/Twitter 的帖子中宣布）。有些人希望用 AI 来运行这个系统，并给予适当的署名，而不是让被引用工作的作者被这堆材料的规模所淹没。也许一项更有价值的工作是找出那些其想法被使用却没有被引用的人。这还不包括那些已经研究并解决了这些问题的人——有时是借助 AI——而他们的工作却没有得到认可。另一些人则希望忽略这些材料，不白白贡献自己的专业知识和时间来帮助这家公司传播这些材料，或者（更可能是）向最初生成这些材料的模型提供反馈以改进它。

人们已经花费了大量笔墨去思考纯数学研究界真正看重的是什么——如果突然有数百个声称的成果砸到我们头上，这其实并不是我们想要的。许多人正确地指出，仅仅知道定理是真还是假，实际上并没有那么有用。这个二元信息之所以有价值，是因为它让人确信确实存在一个（显然）已知的事实，并能让人放手去干。但真正的好处来自对数学的理解，因为它充实了我们的工具箱，触发了与数学其他部分的关联，开启了新的问题等等。但作为局外人，你可能会觉得，说“不，AI 可以说它是真的，但我们想要的是‘理解’这个含糊的概念”，有点像是软弱、反动的借口。实际上，要在纸面上精确界定研究数学中的清晰与理解究竟是什么，是非常困难的。退一步说，评估学生对正在学习并接受考核的数学概念的理解，本身就是一件非常不容易的事，而这些概念是人们已经以某种形式知晓了几个世纪甚至几千年的，评估者（教师、讲师、考官）对它们拥有专业知识、流畅度和精通程度等等。现在试想一下，当某人刚刚综合出一个只有他们（或一小群合作者）才理解的新理论框架时，你该如何评估他对数学的理解？我们究竟通过什么方法才能领会某人对你第一次听到的概念的理解？我认为，答案在于这些概念的交流。

打个比方，当望月新一在 2012 年发布他关于宇宙际泰希米勒理论的四篇论文时，他构建了一个证明 abc 猜想的框架，这份兴奋是真实的，但论文本身的写法无助于传达这些思想。后来举办了研讨会，而面对面交流（通过视频连线）也未能改善局面。撇开实际正确与否不谈，如果该领域的专家因为阐述不清而感到沮丧，无法判断你是否真的证明了那些论断，那就是流程上的失败。我一直以来的观点是，这些论文本可以也应该在随后的几年里被改写得更简单（它们绝对可以做到）也更清晰，以此作为对试图理解它们的学界的一种服务。一个普遍的看法是，如果专家因为论文写得不够清晰而读不懂，那么证明就没有被传达出来，因此该定理就不能被认为已经确立。

我之前就说过，我喜欢这样一个事实：即便是纯数学，实际上也会产生物质产出。对大多数研究而言，这不是图像或实物：被创造出来的东西是写作，是论文，或者有时是黑板演示或幻灯片。我见过的最好的演讲之一，是CT2014上的一场主题演讲，它把报告厅里的黑板用到了极致，演讲的布局和设计恰好一次性用尽了所有可用空间，而演讲后段需要引用的材料就摆在那里，随时可以指过去。遗憾的是，我记不清那人是谁了！幻灯片方面一位杰出的创作者，如果他允许我单独点名的话，是Bryce Clarke（例如，他CT2025演讲的这些幻灯片）。

但总体而言，经受住时间考验的是数学写作。我可以拿起Richard Dedekind 1872年的论文（的译本），它引入了如今被称为戴德金分割的概念来定义实数，而在我看来，它是富有洞见、清晰写作的杰作。我可以读Grothendieck 1957年的Tôhoku论文（尽管我的法语非常贫乏），它的卓越依然闪耀。我曾写道：

数学阐述若要有效，就必须既给出困难思想的直观图景，又给出其含义的精确技术描述。最好的作者能无缝地做到这一点。
——A Crisis of Identification

尽管数学思想会被消化、会经过许多头脑的过滤，阅读旧数学文本仍然值得，这是有原因的。我记得Manjul Bhargava受到阅读Gauss 1801年专著Disquisitiones Arithmeticae的启发，得出了新的洞见，而这些洞见此前只留给那些仅读过下游处理的几代数学家去拾取。数学家的作品质量（在很大程度上）是通过我们的写作来评判的，尽管人们承认，这有时是通过期刊这一代理来完成的，而期刊的审稿人和编辑理想情况下已给了论文最好的机会。也正是这种永久记录，让他们能够创造一份遗产。

所以这把我们带回了那个堆。像上周的许多人一样，我翻看了这份清单，哪怕只是出于好奇。对我来说，一个突出的是黎曼zeta函数临界带中的一致无零点区域，因为我知道我的澳大利亚同事Tim Trudgian及其同事的工作（例如今年3月的这篇论文）是关于获得更大、但仍在衰减的此类区域。另一个是Grothendieck同伦猜想对于从Grothendieck的Pursuing Stacks第一部分中提取出的-群胚版本的建立，那实际上是写给Daniel Quillen的原信。这纯粹从历史角度看很有意思：它确立了Grothendieck对-群胚的定义——实际上几乎没人使用——实际上是正确的。实际证明的结果是一个技术性引理，由Simon Henry猜想，通过一条更长的推理链，足以在这种情形下建立同伦猜想。我要说明，我实际上没有读过其中任何一篇论文，主要是因为它们都不在我实际研究的东西上，也没有近到需要我去读。

既然我们已经确认数学家在意彼此实际写出的内容，那么对于上周出现的700多份PDF文档，我们又该作何评价呢？当然，人们预料到AI会写出垃圾。但你从专家那里得到的，却是针对他们正在审视的材料的这类评价：

我的一位资深同事在那些被解决的问题中发现了自己最喜欢的一个问题，并尝试阅读随附的论文。他告诉我，这篇论文晦涩难懂，如果他作为数学期刊的编辑收到它，“它会直接被扔进垃圾桶”。
——Melissa Lee，莫纳什大学（发表于The Conversation）

还有这个：

我粗略看了一下OpenAI发布的预印本[…]。它很糟糕。它不清晰、混乱，结构也很奇怪。术语“有点不对劲”，有些定理我没想到会被证明，而且表述方式非常奇怪。引理7.4同样不是你在这样的论文中会看到的东西，引理8.1也是如此。
[….]
不，如果这是一篇提交给期刊的学术论文，它应该因质量原因被直接拒稿。作者始终有责任遵守并达到沟通标准。就像一篇用瑞典语写的论文很可能会被《美国数学学会会刊》直接拒稿一样，因为作者有责任让读者能够理解。
——Asaf Karagila（博客文章）

还有这个

“就我所看过的部分而言，我不会花任何钱打赌其中任何一篇有正确的证明。两篇读起来都像如果我是审稿人会立即拒稿的论文，因为两篇似乎主要充斥着对众所周知事实的笨拙证明，没有任何启发性的内容。”
——Nick Kuhn（ALG-TOP邮件列表）

还有这个

但我越想越生气。最让我困扰的是双重标准。

每当我审稿，或收到学生的论文或项目时，我都会采用我们大多数人都会采用的标准。如果一篇论文或学位论文写得如此糟糕，以至于我费了很大劲都读不过第一页，我会拒稿并要求提交一份新的、可读的版本。

对于这些AI生成的论文，我觉得我们作为一个共同体，没有采用同样的质量和严谨标准。它们可以简单地发布多篇100多页的论文，声称解决了这个或那个问题，往往带有冗余的论证、不清晰的逻辑结构、多条死胡同，以及奇怪或令人不安的术语——换句话说，就是垃圾。
——Enrico Fatighenti（自称“不是卢德分子”，在各种任务中使用AI）Proofs and Prompts

还有这个

很明显，许多论文从未经过人工审查：例如，我看了他们的示例#254（一个没有CAT(0)作用的Artin群）：他们的群有116个生成元，但将其输入Astra后，我在10分钟内就得到了一个只有12个生成元的新例子。显然，他们急于发布这个大新闻，重数量而轻质量……为什么？
——Giulio Tiozzo，Proofs and Prompts

当然，也有人愿意无视这些粗制滥造的内容，对他们来说，这些结果太有价值，不容忽视。但事实是，输出内容不可能在原始生成之后经过精炼，而（理想情况下）数学家在自己的成果生成后正是这样做的。一种特别刻薄的观点认为，这就像输出一个庞大的计算，然后把理解的工作留给那些试图从中获取价值的人。事实上，它确实只是一个庞大的计算，只是规模远超任何个人经验，然后被提炼成某种用符号表示的输出，近似于普通写作。

上周在 X/Twitter 上冒出来的恶搞账号 @Endings500 让我觉得很有趣，而当（未形式化的）论文因存在错误而从转储中撤下时，这种乐趣只是微不足道的：

把电影类比拉伸到极限，问题不仅在于有些内容像一部只放映最后 10 分钟的电影，还在于这部电影的质量类似于 Plan 9 from Outer Space（“因其惊人的拙劣而广受赞誉”）。

不过，人们或许可以从以下事实中得到一些安慰：其中一大堆（绝非全部）论断已在 Lean 中形式化。尽管人们从最近的预印本中获益良多，该预印本表明 Navier–Stokes 形式化与描述证明的 pdf 并不匹配，但这其实只是一个概念验证：论文论证的自动形式化确实需要与书面版本进行双重核对，看它们是否匹配，并且应该调整其中之一使它们匹配。在专家检查其中一个或两个之前，这几乎说明不了结果如何。

然而，不需要是 Lean 专家也能看出，像这样的代码（文件 OrdinaryArchimedeanTwistBasic.lean 的全部内容）：

import Mathlib

namespace OAI

noncomputable section
open scoped BigOperators
open MeasureTheory intervalIntegral
open Finset
open Finset Nat ArithmeticFunction
open scoped ArithmeticFunction.Moebius
open Filter
open MeasureTheory Filter
open MeasureTheory
open MeasureTheory Set
open Set MeasureTheory Complex
open Set
open Finset Filter

namespace OrdinaryArchimedeanTwist

end OrdinaryArchimedeanTwist

end

end OAI

实际上什么也没做。这是转储存储库中的一个 Lean 文件（感谢 Lean Zulip 聊天服务器中的 Joseph Meyers 指出其中一些荒谬的文件）。一个基本的确定性代码整洁度检查器就能发现这些问题，更不用说由全能的内部模型对其自身输出进行审计了。Sébastien Gouëzel 在 Lean Zulip 中指出的另一个文件是这样的：

import OAI.Dynamics.TriangleBilliards.SpatialRigidity

namespace OAI

open MeasureTheory Set
open scoped ENNReal symmDiff
noncomputable section
open MeasureTheory Set Filter Function Metric
open scoped Topology Convolution ContDiff
noncomputable section
open MeasureTheory Set
open scoped ENNReal
noncomputable section
open MeasureTheory Set Filter BoundedContinuousFunction
open scoped ENNReal Topology ComplexConjugate
noncomputable section
open MeasureTheory Set Filter
open scoped Topology ComplexConjugate
noncomputable section
open MeasureTheory Filter
open scoped ComplexConjugate
noncomputable section
open MeasureTheory Filter Set
open scoped Topology ComplexConjugate
noncomputable section
open Filter Finset Set
open scoped Topology BigOperators
noncomputable section
open MeasureTheory Filter Set
open scoped Topology ContDiff NNReal
open MeasureTheory Filter Set
open scoped Topology ComplexConjugate
noncomputable section
open Filter Set
open scoped Topology
noncomputable section

同样，这种毫无意义的重复远低于我对自己在本地使用能力较弱的 AI 系统生成 Lean 代码时的预期质量。即使代码能正常编译，这种明显完全缺乏本科水平代码清理的情况也令人震惊。人们或许可以由此推断该系统所产出的英文写作的质量。

如果数学家因其写作而受到评判——写作是交流思想、向他人传达难以描述的理解的媒介——而数学则因其表述的清晰程度而受到评判，那么亲爱的读者，我希望你至少能体会到，为什么转储 700 多份这种性质的长文档不仅令人沮丧，而且侮辱人。