陶哲轩：几周前，AI突破数学形式化临界点

数学界的"最强大脑"，快被AI批量产出的证明淹没了。

菲尔兹奖得主陶哲轩分享了他在IEANTN项目（显式解析数论网络集成项目）中的最新体验：

几周前还需要志愿者花数周才能认领完成的形式化任务，现在AI几小时就能搞定。

一个17世纪数学家帕斯卡就注意到的现象，正在以一种全新的方式困扰着当代数学：

生成一个冗长的正确证明，比生成一个简短的正确证明更容易。

陶哲轩把这个现象称为"阻抗不匹配"，而AI的出现，把这个矛盾推向了极致。

从数周到数小时

陶哲轩主导的

项目，目标很明确：将显式解析数论中大量技术性论文形式化，在Lean证明助手中。

这项工作涉及大量繁琐的数值验证和参数匹配。用陶哲轩自己的话说，

。

按传统方法，他会把单个引理拆分成独立任务发布出去，然后等待志愿者认领——这个过程通常要等好几周。由于人工形式化本身就有难度，志愿者会自然而然地追求证明的简短、高效和自然，提交的代码审查起来也很轻松。

陶哲轩发布的几乎每一个形式化任务，都能在数小时内被AI工具完成。项目中待认领的未解决issue队列，基本清空了。

AI能做局部优化，做不了全局重构

速度的飞跃带来了意想不到的副作用。

AI生成的形式化证明往往比人类写的长出数百行，包含大量冗余步骤，许多引理没有在合适的抽象层次上陈述。单看任何一个证明，好像都不是大问题——毕竟这些证明本来就不是给人读的。但每个臃肿证明都会给项目总构建时间增加几十秒，累积效应变得不可忽视。

陶哲轩把这称为

：证明生成、证明验证、证明消化三个环节之间的速度差距正在拉大。

生成端被AI加速了数个量级，但验证和消化端仍然依赖人类的认知带宽。具体到实践中，将一个包含数千行代码（其中部分由AI生成）的中等规模Lean文档，转化为一个结构优雅、适合提交到Mathlib数学库的版本，成了一项颇具挑战的工作。

陶哲轩发现了当前AI工具的一个清晰边界。

让AI做局部的"code golf"（代码精简），它能胜任，可以把证明的体积压缩一些。

举个例子：发现某个论证在文档中多处重复出现，可以抽象为一个独立引理，而这个引理可能在当前文件之外还有更广泛的用途。陶哲轩指出，他可以先向AI解释这样一个重构方案，AI随后能执行它，但AI无法自发地发现这类重构机会。

AI擅长处理局部的、原子化的任务，但对项目的全局结构缺乏理解。在IEANTN项目的语境下，这意味着AI能快速生成单个引理的证明，却无法判断这个引理应该如何嵌入整个数论估计网络的架构中。

项目推进速度确实比预期快了很多。但陶哲轩表示，他现在需要花更多时间来提前规划形式化任务的scope——预判AI会迅速交回一个证明，因此在发布任务时就要考虑好如何让结果更易审查、更兼容项目的全局结构。

换句话说，瓶颈从"等人来做证明"转移到了"设计好任务，让AI的产出能被有效整合"。数学家的角色正在从亲自执行证明，转向成为证明工程的架构师。要实现这个愿景，每一块拼图都必须在正确的抽象层次、以正确的接口标准存在于系统中。AI能以惊人速度生产拼图块，但拼图块的形状是否与整体蓝图匹配，目前仍然只有人类能判断。

参考链接：

[1]https://mathstodon.xyz/@tao/116789374373843141

[2]https://www.ipam.ucla.edu/news-research/special-projects/integrated-explicit-analytic-number-theory-network/