梦晨 发自 凹非寺 量子位 | 公众号 QbitAI 数学界的"最强大脑"，快被AI出的证明淹没了。 菲尔兹奖得主 陶哲轩 分享了他在IEANTN项目（显式解析数论网络集成项目）中的最新体验： AI生成正确证明的速度太快了，但证明写得太臃肿，人类根本来不及审。 几周前还需要志愿者花数周才能认领完成的形式化任务，现在AI几小时就能搞定。 一个17世纪数学家帕斯卡就注意到的现象正在以全新的方式困扰着当代数学： 生成一个冗长的正确证明，比生成一个简短的正确证明更容易。 陶哲轩把这个现象称为"阻抗不匹配"，而AI把这个矛盾推到了极致。 陶哲轩发布的几乎每一个形式化任务，都能在数小时内被AI工具完成。 项目中待认领的未解决issue队列，基本清空了。 从数周到数小时 陶哲轩主导的 IEANTN 项目，目标是将显式解析数论中大量技术性论文形式化，在Lean证明助手中 建立一个活的、可动态更新的数论估计 网络 。 这个工作涉及大量繁琐的数值验证和参数匹配。 用陶哲轩自己的话说， 这类工作占据了他思考解析数论问题时至少70%的时间 。 按传统方法，他会把单个引理拆分成独立任务发布出去，然后等待志愿者认领——通常要等好几周。 ...