数学界的“最强大脑”陶哲轩最近被AI出的证明淹没了。他在IEANTN项目（显式解析数论网络集成项目）中分享了一个惊人体验：几周前，AI突破数学形式化的临界点，原本需要志愿者花数周才能认领完成的形式化任务，现在AI几小时就能搞定。这个17世纪数学家帕斯卡就注意到的现象——生成冗长正确证明比生成简短正确证明更容易——正以全新方式困扰着当代数学。陶哲轩称之为“阻抗不匹配”，而AI把这个矛盾推到了极致。

IEANTN项目旨在将显式解析数论中大量技术性论文形式化，在Lean证明助手中建立一个活的、可动态更新的数论估计网络。这类工作涉及繁琐的数值验证和参数匹配，据陶哲轩自己说，占据了他思考解析数论问题时至少70%的时间。传统方法是把单个引理拆分成独立任务发布出去，等待志愿者认领，通常要等好几周。但最近几周，自动形式化技术突然跨过临界点，陶哲轩发布的几乎每一个形式化任务，都能在数小时内被AI工具完成，项目中的待认领issue队列基本清空。

速度飞跃带来了意想不到的副作用。AI生成的形式化证明往往比人类写的长出数百行，包含大量冗余步骤，许多引理没有在合适的抽象层次上陈述。单看任何一个证明似乎不是大问题，但每个臃肿证明都会给项目总构建时间增加几十秒，累积效应不可忽视。陶哲轩指出，AI工具当前有一个清晰边界：它能做局部的“code golf”代码精简，把证明体积压缩一些，但全局性的重构决策完全超出其能力范围。比如发现某个论证在文档中多处重复出现可以抽象为独立引理，AI无法自发发现这类机会。

项目推进速度确实比预期快了很多，但陶哲轩表示，他现在需要花更多时间提前规划形式化任务的scope，预判AI会迅速交回证明，因此在发布任务时就要考虑如何让结果更易审查、更兼容全局结构。瓶颈从“等人来做证明”转移到了“设计好任务让AI的产出能被有效整合”。数学家的角色正在从亲自执行证明，转向成为证明工程的架构师。每一块拼图都必须在正确的抽象层次、以正确的接口标准存在于系统中，AI能以惊人速度生产拼图块，但拼图块的形状是否与整体蓝图匹配，目前仍然只有人类能判断。