1.陶哲轩主页
白板在那晚的数学推导中没派上用场陶哲轩盯着屏幕，Lean像刻薄裁判吐出一行行红字反复拉扯后，报错忽然安静1125行Lean代码落定——埃尔德什第613号问题的复杂反例，被逐行核查进了形式化世界写手是ChatGPT，思路由陶哲轩调度，判决由机器拍板。
2.陶哲轩访谈
在一个著名的未解数学问题上，菲尔兹奖得主陶哲轩请出了ChatGPT和数学证明助手Lean，来联手完成一项繁琐而严谨的任务：形式化一个复杂的反例证明。
3.陶哲轩最新成果
这个反例源自保罗·埃尔德什（Paul Erdős）提出的第613号问题，一道困扰数学家几十年的难题。
4.陶哲轩个人主页
https://www.erdosproblems.com/forum/thread/613早在本世纪初，就有数学家给出了一个反例证明，将这一问题「证伪」（也就是找到反例证明原猜想不成立）但把这个证明彻底翻译成计算机可核查的形式却一直没人尝试，因为这意味着要将所有推理细节写成正式的逻辑代码，工作量惊人。
5.陶哲轩导师
而陶哲轩决定尝鲜：让ChatGPT先当他的「翻译官」和「小工」，把人类的纸笔证明转化为Lean语言的严谨代码ChatGPT读论文数学黑话翻译官上线陶哲轩首先让ChatGPT阅读论文中的证明构造论文里的数学描述往往充满符号和行话，但ChatGPT就像一位不知疲倦的助教，可以逐段解释这些构造是什么意思，再尝试用更「机械」的方式表述。
6.陶哲轩讲课
比如，论文构造了一个特殊的图（满足某些顶点与边的计数条件）作为反例，ChatGPT能根据文字描述提炼出关键条件，甚至将它翻译成Lean所需的定义它好比把晦涩的古文译成白话，确保每一步都清晰明了当然，ChatGPT并非真的理解深奥的数学理念，它更多是模式匹配和概率生成。
7.陶哲轩2020
但在这种场景下，它的确展现出惊人的「阅读理解」能力陶哲轩要求它把论文中的命题用Lean语言表述出来，ChatGPT几乎立刻就给出了正确的定义和命题陈述有时候，它甚至会主动「发挥」一下，比如在没有提示的情况下就证明了一个引理的性质。
8.陶哲轩介绍
这种时刻令陶哲轩都感到惊喜，仿佛AI学生一下子开窍了然而兴奋没持续太久，ChatGPT很快卡在了证明的最后一步它能读懂并重述大部分内容，却在真正需要创造性跳跃的地方卡壳毕竟，它不是真正的数学家，只是扮演了一个熟练的翻译加初级解题助手。
9.陶哲轩blog
人机协作1125行代码横空出世接下来就是耐心活：一步一步引导ChatGPT编写Lean代码，也就是所谓「vibe coding」的过程所谓「vibe coding」，指的是人类不给出过于详细的严苛指令，而是凭直觉和整体思路一步步让AI搭建代码，就像即兴合奏一样。
10.陶哲轩资料
在这个过程中，陶哲轩更像一位乐队指挥，提供方向和节奏，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.」（「例如集合{−8, −6, 0, 1, 4}不能如此扩展。
」）
评论(0)