AI携手数学家：陶哲轩引领形式化证明新浪潮

【引言】菲尔兹奖得主陶哲轩借助ChatGPT将深奥的数学论文转化为Lean代码，携手人工智能完成形式化证明。AI虽能解读论文并准确陈述命题，但在关键推理步骤常遇障碍。通过紧密的人机协作，最终产出了1125行经Lean验证的代码。这种名为「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现充当「强大助理」角色，而非独立数学家。

如《自然》杂志每日简报指出，这些工具可助数学家确认近乎不可琢磨的证明、为难题出谋划策，但距自动产出完整新证明尚远。

人类智慧仍不可或缺。至少现时，最精彩创意与洞见，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}不能如此扩展。」）

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