数学界的顶尖天才，正被人工智能批量产出的数学证明淹没——这一趋势正在引发新的挑战。

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

AI生成正确证明的速度确实令人惊叹，但这些证明内容过于冗长，人类审阅者根本来不及处理。

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

一个早在17世纪就被数学家帕斯卡注意到的现象，如今正以全新方式困扰着当代数学界的AI辅助研究：

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

陶哲轩将这个现象称为“阻抗不匹配”，而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/