AI颠覆数学研究！陶哲轩借AI破解数学猜想，形式化成功惊呆数学圈

用AI工具辅助研究数学的项目，再一次被陶哲轩跑通！三周前，他曾发布一篇博文，记录下自己使用Blueprint在Lean4中形式化多项式Freiman-Ruzsa猜想的证明过程。

就在昨天，他激动宣布：将多项式Freiman-Ruzsa猜想的证明形式化的Lean4项目，在三周后取得了成功！现在，依赖关系图已经完全被绿色所覆盖，Lean编译器也报告说，这个猜想完全遵循标准公理。

陶哲轩表示，在整个团队中，自己贡献的代码大概只有5%。这个结果很鼓舞人心，因为这意味着数学家即使不具备Lean编程技能，也能领导Lean的形式化项目。他发现，项目中在数学上最有趣的部分，形式化起来比较容易，而技术上看起来最显而易见的步骤，却最耗时。而使用Blueprint将项目分解成难度小到中等的部分，效果很好，这就让大量并行工作成为可能。这样，许多贡献者就可以处理特定的子任务，而无需理解整个证明过程，甚至可以完全不了解相关的数学领域知识。

与此同时，他在三周前也就是11月18日的那篇博客也被网友翻出，引发热议。

果然，AI加持数学研究颠覆力量的后劲，得需要数月的时间才能让人们认识到。而只有在最前线的研究者，才能在第一时间切实感觉到这种巨大力量的冲击和震撼。

陶哲轩呼吁：数学家们一定要学会用AI了

有网友向陶哲轩提问：这是否意味着，有越来越多的证明是人类不可理解，但机器可解决的？

陶哲轩表示，恰恰相反，如果证明的形式化变得更加主流，并且更多地得到AI辅助，那完全有可能创建出既人类可读、又能被机器阅读的证明。PFR证明的blueprint就证明了这一点——既人类可读，每个证明步骤还带有形式化的理由，还能得到一个依赖关系图，来可视化整个论证的全局结构。

当然，陶哲轩也提醒道，不要把「计算机辅助证明」和「不能提供理解/偶然成立的证明」搞混了。比如对于有限单群分类的超过10000页的证明，几乎百分百是由人工生成的，但一个由计算机协助处理的替代证明，在某些方面看更令人满意。

跟网友经过几轮讨论后，陶哲轩做出以下总结——Blueprint本身就是一种编程语言，可以看作一种Lean的伪代码。许多数学家都应该将写作风格从标准数学英语/LaTex，转换为Blueprint/LaTex。

网友：以后研究都不需要「人类可读」，AI懂就行了

网友表示，陶哲轩对于各种研究工具随意掌握的程度，几乎可以称得上是可怕。

我在研究生阶段对数学的尝试，就就好像一个穴居人本来在摇晃一辆普通的独轮车，忽然眼前出现了一辆直升机，上面的人向我伸出手，告诉我来试试看，一点也不可怕。自从听说四色定理以来，我一直很清楚，形式化是数学的未来。但我没有预料到的是，陶哲轩如此从容不迫，形式化才刚刚获得牵引力，他就能用AI完成几乎所有的数学写作。

形式化，是指从基本公理和规则中真正推导出证明中的每个陈述。而陶哲轩在这篇博文里，把需要死记硬背的劳动都抽象出来，交给了机器。他的工作表明，形式化才刚刚开始在主流数学中受到关注。

已经有人开始畅想：很可能会有一段时间，大多数证明只是在Lean或类似系统中完成，再也没有人需要费心写一篇「人类可读」的论文了。数学，将变成一种编程！