陶哲轩在国际数学家大会讲 AI：AI 证明会越来越多，但数学不会因此变快
- AI 现在真能解出研究级的数学题了：First Proof 拿十道全新问题去测四个 AI 系统，七道题有人答到了可发表的水平。而埃尔德什问题网站上已经堆了近二十份 AI 声称的解答，没有人类专家愿意去验证。题解得出来了，后面几步没跟上。
- 7 月 24 日国际数学家大会的公开讲座上，陶哲轩讲的就是这件事。他不去争论 AI 到底行不行，而是请听众先假设它行，然后问：那我们这行该怎么办。
- 他把数学研究拆成一条流水线：解出证明 → 验证正确 → 写得能读懂 → 被同行接受 → 写进教科书。AI 大幅加速的只有第一步，越往后越慢、越需要人，也越值钱。
- 最反直觉的一条：证明写得太顺滑反而有害。他放了一张自己年轻时批注 Bourgain 1991 年论文的照片，纸上写着「AARGH!」和「我讨厌 Jean Bourgain」。那些卡住人的地方，正是逼读者慢下来真学懂的地方。
- 他给同行的处方是三条：把 AI 使用的披露常态化；把力气从抢着解题转到把证明消化掉；以及最硬的一条：讲不清自己的结果，就不该发表。
AI 已经能解出研究级难题，麻烦从这儿开始
埃尔德什问题网站上，现在堆着几十份 AI 生成的证明。
这些证明里有不少很可能是对的。问题是没人验。
有能力验的人当然存在。难的是没有一个够格的数学家愿意花那个时间，去读一份不知道谁写的、可能几十页长的东西，然后签下自己的名字说「我确认它成立」。有几份提交，连交上来的人自己都写明了：我没有资格判断它对不对。
陶哲轩在讲台上就着这件事问了一句：我们会不会哪天拥有一个被验证过的重大结果的证明，却没有任何一个人类理解到能把它讲清楚？
而 AI 解得出研究级数学题这件事，已经不是设想了。
First Proof 是一个独立的评测项目，专门测 AI 在研究级数学上的真实水平。它的做法是找一批数学家交出自己研究中真实碰到过、已经解出但从未公开发表的问题，网上和文献里都搜不到答案。第二批一共十道题，横跨可计算性理论、离散几何、随机偏微分方程、冯诺依曼代数等方向，五月底在受控条件下交给四个 AI 系统各答一遍，每题只有一次机会，中途不许人插手。答卷送去盲审，约三十位对应领域的专家评审，每份至少两个人看。
其中一道随机偏微分方程的题，有个系统给出的解法跟人类作者的完全不同，评审说印象深刻。
7 月 24 日，费城。四年一届的国际数学家大会正在开会，这是数学界规格最高的场合。陶哲轩做了一场面向公众的讲座，题目是《AI 时代的数学》，52 页幻灯片。
他讲的题目是：AI 已经能做一部分数学了，这一行接下来该怎么办。
关于「AI 到底行不行」，他专门写了一页，然后说今天不谈
他把这个问题写成了一个数学猜想的样子，而且故意留满空格：
在不久的将来某个时候，某些 AI 工具将会，在某种成本下，在某种程度的人类监督下，正确完成某些领域里某些研究级的数学任务，具有某种非平凡的成功率，以及某种程度的正确性和质量。
他说粗糙地分成弱形式和强形式就够用了。这两种情况下，这一行该做的事完全不同：
那大家可以放心地把 AI 当成长期无关紧要的东西，照常过日子。
那想维持现在这套文化和实践就很困难，尤其是当我们把「解出尽可能多的未解问题」当成头号目标的时候。
然后他说，今天这场讲座不谈这个猜想。
他的理由是这场争论已经卡住了。支持和反对的数据点都有一大堆，但大多不是在受控的科学条件下收集的；公开能看到的那些，高度受报道偏差和各种非科学动机的影响，一些关键的成本和变量根本没有披露。他还提醒了一个容易被混过去的区分：一个说法是不是真的，跟我们希不希望它是真的，完全是两回事。
所以他换了个办法：请听众先假设 AI 能做到，把它当作一个前提接受下来。他管这叫「工作假设」，并且专门说明：我不是要求你想要它成立、相信它成立或者接受它成立，这是一个条件分析。支持或反对这个假设的证据，跟我今天要讲的东西是不相干的。
他给这件事的定性是：基础危机，而且是第二次
头一次发生在一百年前。在那之前的几百年里，数学一直靠一套「朴素的」基础在运转：什么是集合、什么是数、什么是无穷、数学的公理到底是哪些，这些问题基本丢给了哲学家。1901 年的罗素悖论和 1931 年的哥德尔不完备定理，逼着一线数学家回过头去查自己一直默认的那些假设。
那三十年动荡，但产出极有价值：一套明确的、严格的、标准化的基础框架。它经受住了严苛的检验，今天仍然是数学可以信赖的工作环境。
陶哲轩说，我们正在进入一个类似的动荡期。上一次要重查的是逻辑地基，这一次轮到了这一行的价值观和干活方式。他也给了同样的结论：等我们把这些东西彻底检查一遍、明确写下来，这个共同体会比以前更强、更有韧性。
AI 能帮你多解题，但多解题真的是目的吗
AI 写得快只是表象。那些证明堵在那儿的真正原因是：「解出一道题」从来就不是这一行唯一要的东西。
陶哲轩在讲座上列了一串做数学研究的理由，多到一张图才装得下：
他说，过去这些目标基本是同向的：在一个上面有进展，通常另外几个也跟着走。所以可以拿其中一两个当其他目标的代理指标，很多目标甚至不必说出口，隐含着就够了。
但所有指标被往死里优化的时候，都会撞上古德哈特定律：一个衡量标准一旦变成大家要冲的目标，它就不再是一个好的衡量标准。
陶哲轩在这里加了一句：生成式 AI 本身是「无根据的」（它的输出不锚定在任何事实上，也没有内在机制保证自己说的话为真），再加上 AI 公司的财务激励，这两样叠在一起，让 AI 工具的使用特别容易触发这条定律。
于是过度的 AI 优化，会让这些原本大体对齐的目标互相发散。他在讲座上是用连着三页的图讲这件事的：
几个目标基本同向。推进其中一个，其余大体跟着走，所以可以拿一两个当其余的代理指标。
同一批目标各走各的。代理指标失效：解题数字上去了，其余几个目标未必跟着动。
这张图值得对着自己所在的行业看一眼。任何一个行业都能列出一串这样的目标，也都习惯了拿其中一两个当其余的代理，因为过去它们确实一起走。而 AI 恰恰最擅长把其中某一个指标单独拉到极高。
那到底该要哪几件事？接下来是全场的主体，陶哲轩当着全场的面，把目标改了五次。
从解题到写进教科书，AI 只加速了第一步
他挑的是「解决问题」这一件事。他特意说明这只是这一行的一个方面，理论建构是同等重要的另一面，需要单独分析，但解题这块最容易被 AI 冲击。
下面这条流水线，就是他改了五次改出来的。点标签看它怎么一步步长出来：
第 1 版：解出尽可能多的未解问题
这个目标听上去没毛病，网络也简单：一头是开放问题，一头是解，中间一根箭头叫「证明生成」。
风险早在 AI 出现之前就知道了：你会收到大量对重大问题的错误解答。任何一个做数论的人都收到过声称证明了黎曼猜想的邮件。
第 2 版：加上「验证它们是对的」
流水线长出第二段：生成出来的先叫「未经验证的解」，验证过了才算数。
这一段 AI 确实帮上了忙。Lean、Rocq、HOL 这类证明助手能把数学证明写成计算机可以逐行核对的代码；让 AI 来做这个翻译，叫自动形式化。
读懂整个论证，判断每一步是否成立。需要一个懂这个方向的专家，花上几天到几周，而且他得愿意为结论署名。
会累，会漏，也会因为「这不算我的研究成果」而根本没人接。
把证明翻译成 Lean 这类语言写的代码，编译器逐行核对，过了就不会有逻辑漏洞。
前提是得先有人（或 AI）完成那次翻译，而翻译本身就是一件很重的活。
陶哲轩说，生成和验证这两端，AI 都已经在很多情况下大幅加速了，而且按工作假设，这个加速还会继续。
然后他抛出那个问题：如果 AI 生成了一份很长的证明，没有人看得懂（包括那个把题目喂给它的人），怎么办？
这就是开头那些堆在埃尔德什问题网站上的东西。机器可能验得过，但没有一个人能站出来说「我懂了，我担保」。
第 3 版：加上「能被清晰地传达和理解」
流水线又长出一段：验证过的解，还得变成「写得好的解」。中间这一步叫证明表述。
而这一步，AI 的表现最奇怪。
写得太顺，读者反而学不会
陶哲轩对当前 AI 写数学的评价是分裂的。
拼写、语法、格式几乎无可挑剔。
他在这里加了个脚注：可以说是太无可挑剔了。
常常在琐碎的地方长篇大论，却飞快掠过、甚至遮蔽了论证里最有趣、最新颖的那部分。
也常常不指出这个结果跟已有文献的关系，不给一个高层次的概览。
同样的观察也出现在别处。First Proof 那批盲审专家的报告里，同一条毛病被反复记录下来：AI 的解答倾向于把例行的部分做得极其细致，却在最难的几步上一笔带过，有时候直接断言某个关键结论「由标准论证即得」，不给理由；有时候引用的论文里根本没有它说的那个结果。
报告里还记了一件更难看的事。有一道题的几份 AI 解答，逐行借用了出题人自己早先那篇论文的措辞，连自造的术语（T-patterns、bends）和公式标号（B、T、D、H）都照搬，却从头到尾没有引用那篇论文一次。评审写下的原话是：如果这是人交上来的，会被判抄袭。
更深一层：表述也会被优化过头
表述是个比验证模糊得多的优化目标。按工作假设，AI 迟早会把表述能力提上去。可即使提上去了，还有一个问题：表述本身也会被过度优化。
一份证明可能被写得太顺滑了：论证里例行的部分和真正困难的部分，被呈现得同样容易消化。
而在人写的证明里，作者当年觉得难的地方，通常会留下某种自然的摩擦：句子变涩，跳步变多，语气变紧。这些痕迹在提醒读者，这儿慢下来，多看两眼。
过度的 AI 润色会把两种摩擦一起抹掉：人为的（作者偷懒、没写清楚），和自然的（这里本来就难）。抹平之后，读者顺顺当当滑过去了，却没有被鼓励去真正理解论证里的关键想法。他用了「悖谬的是」这个说法：人类表述里的那些「瑕疵」，最终可能对读者是有帮助的。
说完这段，他放了一张照片。
这张照片就是那个论点的实物证据。
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 条：
AI 已经能解出研究级数学题，堵住的是后面四步
陶哲轩在国际数学家大会上拆开数学研究的五步流水线，一页带图讲完他讲了什么。
↓ 一页读完 · 有一张会动的图
埃尔德什问题网站（收集数学家埃尔德什留下的一批悬赏难题、公开征解的站点）上，堆着几十份 AI 生成的证明。不少可能是对的，缺的是有人读完、判断它成立、然后签上自己的名字。有几份提交，交上来的人自己都写明没资格判断对错。
而 AI 解得出研究级难题这件事已经落地了。First Proof 是一个独立评测项目，专门找数学家交出自己研究中真碰到过、解出来但从未公开的问题，网上搜不到答案，再在受控条件下交给 AI 系统各答一遍。
数字均出自 First Proof 第二批评测报告与埃尔德什问题网站，陶哲轩 7 月 24 日在费城的国际数学家大会公开讲座上只引了结论。他绕开「AI 到底行不行」的争论，请听众先假设它行，再问这一行该怎么办。
陶哲轩列了一串做数学的理由：解未解问题、建立理论、理解世界、建共同体、训练下一代、留下有持久审美价值的作品。过去这些目标大体同向，推一个，其余跟着走，所以拿解题数量当其余目标的代理指标也没出过事。
古德哈特定律讲的就是接下来这一步：一个衡量标准一旦变成大家要冲的目标，它就不再能衡量原来那件事。他补了一句，生成式 AI 的输出不锚定在任何事实上，再加上 AI 公司的财务激励，让这条定律格外容易被触发。
他从「解出尽可能多的未解问题」出发，每发现一个漏洞就往目标里加一句：还得验证是对的；还得能被人读懂；还得被同行消化和接受；最后还得进入这个领域的定论理论（他叫经典化，也就是写进权威教科书、成为下一代学生学到的标准说法）。改五次，一条五步流水线就长了出来，每加一格，AI 能替人干的那截就往前缩一格。
他对 AI 写数学的评价分成两半：拼写、语法、格式几乎无可挑剔，脚注里他补了一句「可以说是太无可挑剔了」；同时它常在琐碎处长篇大论，飞快掠过甚至遮蔽掉论证里最新颖的那部分，不给高层概览，也不交代这个结果跟已有文献什么关系。First Proof 的盲审专家独立记下了同一条毛病：关键步骤一句「由标准论证即得」带过；有几份解答逐行借用出题人早年论文的措辞和记号，却一次没引用，评审写下的原话是，人交这稿会判抄袭。
再深一层：人写的证明里，作者当年觉得难的地方会留下摩擦，句子变涩、跳步变多。这些痕迹在提醒读者，这儿慢下来。过度润色把它们一起抹平，例行的部分和真正困难的部分被呈现得同样容易消化。
他推荐莱顿声明作为起点（一份 6 月 2 日上线的数学界 AI 使用倡议，由十六位数学家起草，已获国际数学联盟背书），从中取了操作层面的四条：披露工具使用、支持评审的需要、正确性责任在人类作者、在正确归属上下功夫。声明本身还有监管、伦理、产业章节，这场讲座没取。
抢在别人前面把题解出来。
写清楚、评审、写进教科书这些活，常被认为不如生成证明有声望，靠人类编辑和审稿人自愿服务。
降低对生成和「第一个解出来」的强调，提高对证明消化的强调，表述、发表、经典化。
把负责任的披露常态化，避免最坏的情况：偷偷用 AI 又藏着以免挨批。
拇指规则：讲不清自己的结果，就不该发表。
他自己在幻灯片上做了两次披露，都搁在页脚：所有破折号是人工敲的；本幻灯片用了 AI 补全文字和生成图表。同样的分析，他说还需要在教学、指导学生、招聘、经费申请、公众传播上各做一遍。
没人肯签字！
至少一个 AI 系统
答到了能发表
的水平
今天不吵。
该怎么办？
再回来问这个问题。
改写了五次
流水线就这么
长出来了
挑不出毛病，
这也算坏事？
- × 堵在验证前
- × 堵在写清楚前
- × 堵在评审前
- × 堵在进教科书前
数学没跟着快。
该干什么？
就别发表。
那几步靠人