AI 能帮你多解题，但多解题真的是目的吗

AI 写得快只是表象。那些证明堵在那儿的真正原因是：「解出一道题」从来就不是这一行唯一要的东西。

陶哲轩在讲座上列了一串做数学研究的理由，多到一张图才装得下：

他说，过去这些目标基本是同向的：在一个上面有进展，通常另外几个也跟着走。所以可以拿其中一两个当其他目标的代理指标，很多目标甚至不必说出口，隐含着就够了。

但所有指标被往死里优化的时候，都会撞上古德哈特定律：一个衡量标准一旦变成大家要冲的目标，它就不再是一个好的衡量标准。

陶哲轩在这里加了一句：生成式 AI 本身是「无根据的」（它的输出不锚定在任何事实上，也没有内在机制保证自己说的话为真），再加上 AI 公司的财务激励，这两样叠在一起，让 AI 工具的使用特别容易触发这条定律。

于是过度的 AI 优化，会让这些原本大体对齐的目标互相发散。他在讲座上是用连着三页的图讲这件事的：

这张图值得对着自己所在的行业看一眼。任何一个行业都能列出一串这样的目标，也都习惯了拿其中一两个当其余的代理，因为过去它们确实一起走。而 AI 恰恰最擅长把其中某一个指标单独拉到极高。

那到底该要哪几件事？接下来是全场的主体，陶哲轩当着全场的面，把目标改了五次。

从解题到写进教科书，AI 只加速了第一步

他挑的是「解决问题」这一件事。他特意说明这只是这一行的一个方面，理论建构是同等重要的另一面，需要单独分析，但解题这块最容易被 AI 冲击。

下面这条流水线，就是他改了五次改出来的。点标签看它怎么一步步长出来：

第 1 版：解出尽可能多的未解问题

这个目标听上去没毛病，网络也简单：一头是开放问题，一头是解，中间一根箭头叫「证明生成」。

风险早在 AI 出现之前就知道了：你会收到大量对重大问题的错误解答。任何一个做数论的人都收到过声称证明了黎曼猜想的邮件。

第 2 版：加上「验证它们是对的」

流水线长出第二段：生成出来的先叫「未经验证的解」，验证过了才算数。

这一段 AI 确实帮上了忙。Lean、Rocq、HOL 这类证明助手能把数学证明写成计算机可以逐行核对的代码；让 AI 来做这个翻译，叫自动形式化。

陶哲轩说，生成和验证这两端，AI 都已经在很多情况下大幅加速了，而且按工作假设，这个加速还会继续。

然后他抛出那个问题：如果 AI 生成了一份很长的证明，没有人看得懂（包括那个把题目喂给它的人），怎么办？

这就是开头那些堆在埃尔德什问题网站上的东西。机器可能验得过，但没有一个人能站出来说「我懂了，我担保」。

第 3 版：加上「能被清晰地传达和理解」

流水线又长出一段：验证过的解，还得变成「写得好的解」。中间这一步叫证明表述。

而这一步，AI 的表现最奇怪。

写得太顺，读者反而学不会

陶哲轩对当前 AI 写数学的评价是分裂的。

同样的观察也出现在别处。First Proof 那批盲审专家的报告里，同一条毛病被反复记录下来：AI 的解答倾向于把例行的部分做得极其细致，却在最难的几步上一笔带过，有时候直接断言某个关键结论「由标准论证即得」，不给理由；有时候引用的论文里根本没有它说的那个结果。

报告里还记了一件更难看的事。有一道题的几份 AI 解答，逐行借用了出题人自己早先那篇论文的措辞，连自造的术语（T-patterns、bends）和公式标号（B、T、D、H）都照搬，却从头到尾没有引用那篇论文一次。评审写下的原话是：如果这是人交上来的，会被判抄袭。

更深一层：表述也会被优化过头

表述是个比验证模糊得多的优化目标。按工作假设，AI 迟早会把表述能力提上去。可即使提上去了，还有一个问题：表述本身也会被过度优化。

一份证明可能被写得太顺滑了：论证里例行的部分和真正困难的部分，被呈现得同样容易消化。

而在人写的证明里，作者当年觉得难的地方，通常会留下某种自然的摩擦：句子变涩，跳步变多，语气变紧。这些痕迹在提醒读者，这儿慢下来，多看两眼。

过度的 AI 润色会把两种摩擦一起抹掉：人为的（作者偷懒、没写清楚），和自然的（这里本来就难）。抹平之后，读者顺顺当当滑过去了，却没有被鼓励去真正理解论证里的关键想法。他用了「悖谬的是」这个说法：人类表述里的那些「瑕疵」，最终可能对读者是有帮助的。

说完这段，他放了一张照片。

幻灯片第 33 页。陶哲轩给这张照片的说明只有一句：「一篇 1991 年 Bourgain 的论文，被年纪小得多的我批注过。」Jean Bourgain 是比利时数学家、菲尔兹奖得主，调和分析领域的大家，2018 年去世。

同一页的局部放大（本站截取）。印刷体那句「We skip the details.」（细节我们略过）被划了一道横线，横线下面写着 AARGH!；右边是三个大问号，再往右是「Sobolev norms!」；上面那行手写是 「I hate Jean Bourgain.」（我讨厌 Jean Bourgain。）

这张照片就是那个论点的实物证据。

Bourgain 写下「细节我们略过」，年轻的陶哲轩读到这儿卡死了。他划线、打问号、写下「Sobolev norms!」提醒自己该往哪个方向想，最后在页边上写了一句「我讨厌 Jean Bourgain」。

三十多年后，他把这一页拍下来，放到国际数学家大会的屏幕上。正是这些卡住他的地方，逼着他慢下来，把那套东西真的学会了。一份每一步都同样顺滑的证明，不会给读者留下这样的位置。

紧接着他引了 William Thurston 1994 年那篇《论数学中的证明与进步》里的一段：

我们不是在完成某种抽象的、关于定义、定理和证明的生产配额。衡量我们成功与否的标准，是我们所做的事情能否让人们更清晰、更有效地理解和思考数学。

William Thurston，《On proof and progress in mathematics》，1994

证明多了，数学却没有变快

写得让人看懂，还只是第三步。

第 4 版：加上「被共同体消化和接受」

一份证明要真的对这个领域有贡献，光是正确、易读还不够。别的数学家得消化它，把它吸收进自己的工作里。

作者能帮上忙：讲讲自己当初卡在哪、怎么想通的、为什么选这条路，这些东西能让别人更快吃下去。但当前的 AI 工具对自己的求解过程相当不透明，那些内部运作属于商业机密的专有模型尤其如此。

而共同体接受这件事，本质上是慢的、人的。好的表述和仔细的写作能促进它，但它终究是一个外部过程，没法由作者和他手上的 AI 单方面优化完成。

这套东西现在靠什么运转？靠人类编辑和审稿人自愿提供服务。陶哲轩点了一句：这份工作常被认为不如生成证明那么有声望，但它是不可或缺的一环，是把数学家的个人成就转化成集体进步和理解的方式。

AI 可以在这里当过滤器，比如期刊可以自动退掉那些被标记为验证不充分或表述不合格的稿子。但过滤器替代不了接受本身。

第 5 版：加上「被纳入这个领域的定论理论」

就算发表了，也不总是一个解的终点。关键结果最终要进入这个学科的权威教科书和参考资料，成为教给下一代学生的标准说法。陶哲轩管这一步叫经典化（canonicalization）。

这是所有阶段里最慢的一个，需要整个共同体广泛的、审议式的共识，也是最不适合被 AI 优化的一个。

但他说，它是整个流程里最有价值的部分。理由有两条。第一，很多应用只有在底层数学被彻底消化之后才变得可行。第二条更要紧：AI 工具今天在数学上的成功，恰恰关键性地依赖于人类数学家几个世纪里辛苦建立起来的那些经典理论。模型能解题，是因为前人已经把这一行整理成了它学得动的样子。

五步走完，诊断也就出来了

如果 AI 真能干这些活，而政策和文化不做相应改变，这条流水线上到处都会出现「阻抗失配」（impedance mismatch）。这是个电路里的词，指两段线路接口对不上，能量卡在接缝处过不去。他也用了一个更直白的说法：证明消化不良。

具体是四处堵：

一句话：我们将从证明稀缺的时代，转入证明过剩的时代。

这些迹象已经在出现了。他说，事实上早在现代 AI 出现之前，压力就已经在积累。

他自己用过一个更好懂的类比

三个月前，他在社交账号上把这条流水线换成了做饭：

在同一串帖子里，他给了一个观察，比幻灯片上任何一句都更直接：证明生成这一端的大规模加速，实际上并没有带来数学进展本身的显著加速。

他还提到一个副作用：一个问题被 AI「解决」了却没人看得懂，反而可能扼杀掉别人继续研究它的兴趣。毕竟它已经「解决」了，尽管没有任何人类理解那个解。

那数学家该干什么

既然堵在后面几步，力气就该换个地方花。

他推荐莱顿声明作为起点。这份倡议今年 6 月 2 日上线，起点是 2025 年 9 月在莱顿大学的一次研讨会，由十六位数学家组成的工作组起草，成员来自剑桥、哥伦比亚、牛津、莱顿、苏黎世联邦理工等机构。它已经得到国际数学联盟的背书，也就是主办这次大会的同一个组织。

陶哲轩从声明里挑了四条，配了三句自己的评论。

需要说明的是，莱顿声明本身比陶哲轩取用的这四条宽得多。它还有专门章节谈 AI 用于战争、大规模监控、破坏民主和环境代价，呼吁加强对 AI 产业的公共监督，其中给政策制定者的一条直接叫「别信炒作」。这场讲座只取了操作层面的部分。他讲的是数学共同体自己该怎么干活。

他自己在幻灯片上做了两次披露

第一页的脚注写着：这些幻灯片里所有的破折号都是人工敲的。（长破折号现在常被当成 AI 写作的标记。）

讲到「把披露常态化」那一页，脚注写着：本幻灯片使用了 AI 工具来自动补全文字和生成图表。

两句都没放进正文，就搁在页脚。

最后

他说解题只是一个方面。同样的分析还需要在教学、指导学生、招聘、经费申请、公众传播上各做一遍。在一些领域（尤其是教育和训练），需要强调工作中人的那一面，严格限制 AI 工具的使用；在另一些领域，则需要主动出击，按我们自己的条件去定义怎么把这些工具纳入工作流。还需要新的工作流和新的基础设施来补充传统的那些，但那是另一场讲座。

他留给全场的最后一句是：我们的共同体需要坐到一起，就 AI 能力和我们的目标与价值观，进行开放而诚实的讨论。

正文的最后一页，他没有再加评论，只放了莱顿声明的第 7 条：

幻灯片第 51 页，整场正文的最后一页，画面上只有这一条，没有配任何文字。中文见下。

他在台上列了一串做数学的理由：解未解问题、建立理论、应用知识、建立共同体、训练下一代、创造有持久审美价值的作品。过去这些目标基本同向，推一个另几个也跟着走，所以可以拿其中一两个当其余的代理指标。

问题出在指标被往死里优化的时候。生成式 AI 的输出不锚定在任何事实上，也没有内在机制保证自己说的话为真，再叠上 AI 公司的财务激励，这两样让它特别容易把某一个指标单独拉到极高，其余的原地不动。

这张对照值得对着自己的行业看一眼：任何一行都能列出一串这样的目标，也都习惯了拿一两个当其余的代理。

他当场把「解出尽可能多的未解问题」这个目标改了五次。每加一条要求，流水线就长出一段，而 AI 能替人干的那截就往前缩一格。这是全篇最该带走的东西。

陶哲轩对 AI 写数学的评价是分裂的：拼写语法格式几乎无可挑剔，他在脚注里加了一句「可以说是太无可挑剔了」；但常在琐碎处长篇大论，飞快掠过甚至遮蔽了论证里最有趣、最新颖的那部分，也不指出跟已有文献的关系。First Proof 的盲审报告独立记下了同一条毛病：关键步骤一句「由标准论证即得」带过；有几份逐行借用出题人早先论文的措辞和自造术语却一次没引用，评审的原话是「如果这是人交上来的，会被判抄袭」。

左边那句手写批注是真的。他在幻灯片上放了一张自己年轻时批注 Bourgain 1991 年论文的照片：印刷体「细节我们略过」被划了一道线，下面写着 AARGH，旁边三个问号，上一行是「我讨厌 Jean Bourgain」。三十多年后他把这一页拍下来放上大会屏幕，正是这些卡住他的地方，逼他慢下来把那套东西真的学会了。

后两步最慢：同行接受靠人类编辑和审稿人自愿服务，这活常被认为不如生成证明有声望，却是把个人成就转成集体进步的方式；经典化最慢，需要整个共同体的审议共识，也最不适合被 AI 优化，但它最值钱，AI 今天能解题，恰恰是因为前人几个世纪把这行整理成了它学得动的样子。四处都会堵：等人验证、等人写清楚、评审被数量压垮、多到没法整合成定论。这行会从证明稀缺转入证明过剩。

数字是谁测的：7/10 出自 First Proof 第二批报告（约 30 位领域专家双盲评审），埃尔德什问题积压量与所有观点均出自陶哲轩本人的讲座与 Mastodon 帖子。需要说明的是，他本人是受测的四个系统之一（UCLA Moonshot Harness）的团队成员，幻灯片中未提及这一点。