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

数学界的“最强大脑”，快被AI出的证明淹没了。

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

AI生成正确证明的速度太快了，但证明写得太臃肿，人类根本来不及审。

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

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

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

陶哲轩把这个现象称为“阻抗不匹配”，而AI把这个矛盾推到了极致。

从数周到数小时

陶哲轩主导的IEANTN项目，目标是将显式解析数论中大量技术性论文形式化，在Lean证明助手中建立一个活的、可动态更新的数论估计网络。

这个工作涉及大量繁琐的数值验证和参数匹配。

用陶哲轩自己的话说，这类工作占据了他思考解析数论问题时至少70%的时间。

按传统方法，他会把单个引理拆分成独立任务发布出去，然后等待志愿者认领——通常要等好几周。

由于人工形式化本身困难，志愿者会自然而然地追求证明的简短、高效和自然，提交的代码审查起来也很轻松。

但在最近几周，自动形式化技术突然跨过了某个临界点。

陶哲轩发布的几乎每一个形式化任务，都能在数小时内被AI工具完成。

项目中待认领的未解决issue队列，基本清空了。

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

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

AI生成的形式化证明往往比人类写的长出数百行，包含大量冗余步骤，许多引理没有在合适的抽象层次上陈述。

单看任何一个证明，好像都不是大问题，因为这些证明本来就不是给人读的。

但每个臃肿证明都会给项目总构建时间增加几十秒，累积效应变得不可忽视。

陶哲轩把这称为“阻抗失配”：证明生成、证明验证、证明消化三个环节之间的速度差距正在拉大。

生成端被AI加速了数个量级，但验证和消化端仍然依赖人类的认知带宽。

具体到实践中，将一个包含数千行代码（其中部分由AI生成）的中等规模Lean文档，转化为一个结构优雅、适合提交到Mathlib数学库的版本，成了一项颇具挑战的工作。

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

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

但全局性的重构决策，完全超出了现有AI工具的能力范围。

比如发现某个论证在文档中多处重复出现，可以抽象为一个独立引理，而这个引理可能在当前文件之外还有更广泛的用途。

陶哲轩指出，他可以向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/

本文来自微信公众号“量子位”，作者：梦晨，36氪经授权发布。