陶哲轩，用AI爆改科研范式

新智元报道

编辑：艾伦

【新智元导读】陶哲轩让ChatGPT把复杂的数学论文翻译成Lean代码，与AI合作完成形式化证明。AI能理解论文、写出正确命题，却常在关键处卡壳。经过人机配合，终于生成1125行被验证的证明。这种「vibe coding」式合作，也让数学家重新思考：AI或许不是独立的解题者，却正在深刻改变数学研究的工作方式。

白板在那晚的数学推导中没派上用场。

陶哲轩盯着屏幕，Lean像刻薄裁判吐出一行行红字。

反复拉扯后，报错忽然安静。

1125行Lean代码落定——埃尔德什第613号问题的复杂反例，被逐行核查进了形式化世界。

写手是ChatGPT，思路由陶哲轩调度，判决由机器拍板。

在一个著名的未解数学问题上，菲尔兹奖得主陶哲轩请出了ChatGPT和数学证明助手Lean，来联手完成一项繁琐而严谨的任务：形式化一个复杂的反例证明。

这个反例源自保罗·埃尔德什（Paul Erdős）提出的第613号问题，一道困扰数学家几十年的难题。

https://www.erdosproblems.com/forum/thread/613

早在本世纪初，就有数学家给出了一个反例证明，将这一问题「证伪」（也就是找到反例证明原猜想不成立）。

但把这个证明彻底翻译成计算机可核查的形式却一直没人尝试，因为这意味着要将所有推理细节写成正式的逻辑代码，工作量惊人。

而陶哲轩决定尝鲜：让ChatGPT先当他的「翻译官」和「小工」，把人类的纸笔证明转化为Lean语言的严谨代码。

ChatGPT读论文

数学黑话翻译官上线

陶哲轩首先让ChatGPT阅读论文中的证明构造。

论文里的数学描述往往充满符号和行话，但ChatGPT就像一位不知疲倦的助教，可以逐段解释这些构造是什么意思，再尝试用更「机械」的方式表述。

比如，论文构造了一个特殊的图（满足某些顶点与边的计数条件）作为反例，ChatGPT能根据文字描述提炼出关键条件，甚至将它翻译成Lean所需的定义。

它好比把晦涩的古文译成白话，确保每一步都清晰明了。

当然，ChatGPT并非真的理解深奥的数学理念，它更多是模式匹配和概率生成。

但在这种场景下，它的确展现出惊人的「阅读理解」能力。

陶哲轩要求它把论文中的命题用Lean语言表述出来，ChatGPT几乎立刻就给出了正确的定义和命题陈述。

有时候，它甚至会主动「发挥」一下，比如在没有提示的情况下就证明了一个引理的性质。

这种时刻令陶哲轩都感到惊喜，仿佛AI学生一下子开窍了。

然而兴奋没持续太久，ChatGPT很快卡在了证明的最后一步。

它能读懂并重述大部分内容，却在真正需要创造性跳跃的地方卡壳。

毕竟，它不是真正的数学家，只是扮演了一个熟练的翻译加初级解题助手。

人机协作

1125行代码横空出世

接下来就是耐心活：一步一步引导ChatGPT编写Lean代码，也就是所谓「vibe coding」的过程。

所谓「vibe coding」，指的是人类不给出过于详细的严苛指令，而是凭直觉和整体思路一步步让AI搭建代码，就像即兴合奏一样。

在这个过程中，陶哲轩更像一位乐队指挥，提供方向和节奏，ChatGPT则即兴「演奏」出代码片段。

Lean充当严格的裁判，每写一段就立刻检查对不对，如果不对，报错信息就是「音准」偏了，需要调整。

这一人机协作的体验既神奇又让人啼笑皆非。

ChatGPT有时展现出高超的「琴技」：它居然能猜出数学家想要证明的中间引理，并直接给出对应的Lean证明思路！

很多常规定义、基本引理，它张口就来，速度飞快。

这让陶哲轩省去了大量查阅Lean库和语法的时间，等于身边多了个熟悉Lean语言的超级速记员。

然而，当涉及比较复杂或微妙的地方，AI就开始「跑调」了：经常写出一长串Lean代码却无济于事，不是逻辑不通就是和之前的定义对不上。Lean会毫不留情地报错，而ChatGPT有时还一脸无辜地看不出错在哪，需要人类耐心指正。

AI不断绕弯子，不是遗忘前提，就是引错定理，把简单问题搞得扑朔迷离。

陶哲轩不得不一次次提示：「嘿，你该证明的是这个基本性质，别走远了。」

就这样来回拉锯，才终于把这个「小目标」攻克。

经过将近一周的「磨炼」，ChatGPT和陶哲轩终于完成了整个反例证明的形式化。

Lean代码整整1125行，俨然一部迷你巨著。

https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/erdos_613.lean

回头看这些代码，作者笑称完全是一坨「意大利面条代码」——结构盘根错节，充满了AI生成的冗长绕行和中途更改的思路。

正常情况下，程序员看到这样的代码可能要头疼不已；但在数学证明里，这反倒不是什么大问题。

因为Lean最终验证通过了，就意味着每一句话、每一个推理步骤在逻辑上都是正确的。

就算代码看起来冗繁，只要能被Lean接受，那证明就在严谨意义上成立了。

正如陶哲轩所说，Lean简直是「vibe coding」的宏大舞台。

AI闹乌龙，人类擦屁股

谁更耗时间？

可能有人会问：让AI瞎折腾一通，吐出上千行絮絮叨叨的代码，这真的省时间吗？

陶哲轩的回答是肯定的。

虽然和ChatGPT互动有时让人抓狂，但对比他亲自动手从零写这1125行Lean证明，AI至少帮他节省了一半以上的时间和精力。

更有趣的是，ChatGPT在对话中还能及时发现陶哲轩提要求时的一些小错误，比如参数取值不当等，然后自动纠正再生成代码。

它不仅是听话的码农，偶尔还兼职「质检」，替人类把关。

这种体验让陶哲轩直呼过瘾——过去觉得不值得一试的繁琐计算，现在敢放心交给AI跑，他则专注于更有创意的部分。

当然，并不是说AI已经万能。

其实在正式编写Lean证明的过程中，大量低级而重复的收尾工作最后还是人类在做。

ChatGPT写出的代码片段往往需要陶哲轩仔细检查、微调格式，然后粘贴进Lean运行，看是否通过。

一旦报错，再回头提示ChatGPT修改。

许多时候AI会陷入一个狭窄思路，不停产出同样错的代码，需要人类耐心引导它跳出死循环。

这一切都说明，AI目前充当的是「能力强大的助理」角色，而非独立的数学家。

正如Nature杂志的每日简报所指出，这些工具可以帮助数学家确认某些近乎不可琢磨的证明、为困难问题出谋划策，但离自动产出完整新证明还有距离。

人类的智慧仍是不可或缺的。至少现在来看，最精彩的创意和洞见，AI还给不出来。

{1, 2, 4, 8, 13}推翻了Erdős猜想

另一则引发轰动的案例发生在Erdős第707号问题上。

这道问题关乎组合数学中的Sidon集合与完美差集的关系——听上去高深莫测，但简单来说，Erdős猜想任何一个特殊的「Sidon数集」都能扩充成某种「完美差集」。

这个猜想悬而未决几十年，奖金为1000美元。

直到最近，两位数学家鲍里斯·阿列克谢夫（Boris Alexeev）和达斯汀·米克森（Dustin G. Mixon）找到了令人意外的反例：集合{1, 2, 4, 8, 13}就是一个无法扩充成完美差集的Sidon集！

五个看似普通的数字，就这样终结了一个长期悬而未决的猜想，令数学界既兴奋又惊讶。

发现反例只是故事的一半。

这两位研究者做了一个大胆决定：让AI来验证他们的发现。

他们听说陶哲轩成功用ChatGPT编写Lean证明，于是如法炮制，请出最新的大模型来协助，把反例证明从头到尾写成Lean代码。

他们不仅形式化了自己找到的新反例，还让AI把几十年前一位数学家马歇尔·霍尔（Marshall Hall Jr.）曾给出的另一个反例也写成Lean证明。

其实霍尔的结果早在1940年代就发表了，但长期被学界忽视了。

Marshall Hall Jr. 在 1947 年的论文《Cyclic projective planes》（Duke Math. J. 14(4): 1079–1090）里，在定理 4.3 后的下一段，给出了不能扩展为任何有限完美差集（λ=1 的差集，亦称平面差集）的具体反例。

原文里他举的例子就是：

For example the set {−8, −6, 0, 1, 4} may not be so extended.

https://projecteuclid.org/journals/duke-mathematical-journal/volume-14/issue-4/Cyclic-projective-planes/10.1215/S0012-7094-47-01482-8.short

这一切听起来就像让AI一边考古、一边盖新楼——把人类数学遗产用现代工具重做一遍，以确保万无一失。

结果如何呢？

ChatGPT不负众望，经过无数次人机对话和尝试，最终吐出了长达数千行的Lean证明代码，把新旧两个反例案例统统严丝合缝地验证了一遍。

论文作者感叹：「正式证明几乎每一行都是ChatGPT写的」。

可以说，没有AI帮忙，这样繁琐的形式化工作几乎不可能在短时间内完成。

这也是他们为何在论文初稿中大胆署名ChatGPT和Lean为共同作者的原因——一个写了证明，一个审了证明。

这一举动由于arXiv的规定，最后发表时还是去掉了AI作者的名字。

更令人好奇的是，他们采用的也是类似「vibe coding」的交互式编程方式。

不是预先设计好完整证明步骤，再让AI去填空，而是边想边让AI试，一步步把想法转化为代码。

这样做的好处是人类不需要过多操心Lean的语法细节，而由AI根据上下文「自由发挥」提案，然后人类再筛选纠正。

这种人机协作方式颇有即兴创作的味道：AI提供源源不断的灵感火花，人类负责辨别哪些是宝石、哪些只是火花。

然而这种自由也带来了大量「垃圾代码」和反复尝试。

作者直言，最终的Lean证明简直是一锅夹生的「意大利面」，里面充满了AI走弯路留下的冗余逻辑。

好在有Lean这个「蜻蜓队长」把关，每个步骤都严格审核，否则真不敢相信AI产出的证明就一定可靠。

正如两位作者所强调的，大模型常常幻觉、出错，如果没有形式化验证（如使用Lean），根本无法信任这样的证明。

AI+人类

数学证明的新范式

AI与人类在数学中协作的艺术想象。

国外权威媒体也开始关注这一趋势：数学证明正悄悄进入「AI辅助时代」。

Quanta Magazine就报道了数学家们对于AI助手的看法，许多人已经在为这种范式转变做准备，思考在AI时代如何重新定义「证明」。

毕竟从历史看，每当出现新工具，数学家的工作方式就会随之改变：计算器、计算机代数系统，现在轮到了智能AI。

即使只能把证明中枯燥繁琐的部分外包给AI，也将「极大改变我们从事数学的方式」。

的确，当人类不再需要手动检查每个细节，就能把更多精力放在创造性的思考上。

另一方面，也有数学家提出谨慎的声音。

蒙特利尔大学的安德鲁·格兰维尔（Andrew Granville）坦言，他担心过度依赖AI验证会让研究者失去锻炼思维的机会：

真正的理解往往来自于亲自动手，「弄脏双手」。

Andrew Granville

这种顾虑不无道理：如果AI成了拐杖，年轻一代会不会变得不善于独立证明？

然而，多数专家认为，与其抗拒AI，不如主动拥抱、学习驾驭。

毕竟纸和铅笔的时代早已过去，电脑验算、机器证明正成为新常态。

未来的数学家或许更像是总指挥，调度AI这个强大的工具完成证明，就像科学家使用实验仪器那样。

陶哲轩把这种前景称作「数学的工业化时代」，要用AI扩充数学家的能力版图。

一如当年国际象棋出现计算机助手，顶尖棋手学会与电脑共舞，开辟出人机融合的新境界。

数学领域如今也站在类似的门槛上：AI不会取代数学家，但正在成为数学家工作桌上的标配工具。

也许若干年后，我们回顾这段历史时，会惊叹地发现：正是从ChatGPT与Lean的「合奏」开始，证明的方式被重新定义，人类对真理的探索奏响了新的乐章。

在AI的陪伴下，数学家的征途不再是孤军奋战，而更像是一场人与机器联袂出演的华丽冒险。

定理未必更容易求证了，但证明的旅程，变得前所未有的精彩。

参考资料：

https://arxiv.org/abs/2510.19804

https://mathstodon.xyz/@tao/115493667607261044

https://www.quantamagazine.org/mathematical-beauty-truth-and-proof-in-the-age-of-ai-20250430

https://www.zhihu.com/question/4991950322