AI与数学家合作：1125行代码完成复杂证明

【导读】陶哲轩与ChatGPT携手，将复杂的数学论文转化为1125行被验证的Lean代码，展现了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并非真的理解深奥的数学理念，它更多是模式匹配和概率生成。

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

人机协作的“vibe coding”

接下来就是耐心活：一步一步引导ChatGPT编写Lean代码。所谓「vibe coding」，指的是人类不给出过于详细的指令，而是凭直觉和整体思路一步步让AI搭建代码。

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

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

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

AI与人类协作的未来

可能有人会问：让AI折腾出上千行代码，真的省时间吗？

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

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

另一则案例发生在Erdős第707号问题上。两位数学家利用AI验证了他们的发现，成功形式化了新旧两个反例的Lean证明。

AI+人类：数学证明的新范式

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