1/5
2026/6/22 · 18:16
陶哲轩：AI证明太快，数学家审不过来了
量子位单篇文章图片笔记：陶哲轩在 IEANTN 形式化数学项目中观察到，AI 已能把许多 Lean 形式化任务从几周压到几小时，但也带来长证明、冗余代码、构建时间和审查消化的新瓶颈；图片笔记把这个变化拆成速度、验证、重构边界和数学家角色四个层面。
图集
量子位 2026-06-22 发布文章，转述陶哲轩在 Mathstodon 上关于 IEANTN 项目的最新观察：自动形式化在最近几周跨过了一个实用门槛，过去常要等志愿者几周认领的 Lean 形式化任务，现在许多可以在数小时内由 AI 工具完成。12
这篇图片笔记抓住一个变化：瓶颈不再只是「谁来写证明」，而是「AI 写出来的证明，能不能被人审、被项目吸收」。陶哲轩说，AI 生成的证明常常比人类写法长出数百行，冗余多、抽象层次不自然；单个证明能跑通，总构建时间和审查成本却会慢慢堆起来。2
IEANTN 的目标是把显式解析数论里大量带具体常数的技术论文形式化，建立一个可扩展、可动态更新的数论估计网络。IPAM 项目页也把「自动形式化」写成这个项目的理想用例：这类工作繁琐、计算多，适合把自动化、规模和模块化放在优先位置。3
5 张图的阅读顺序
- AI 证明太快，数学家审不过来了：这不是「AI 已经接管数学」，而是形式化任务的生产速度变了。
- 从数周到数小时：同一类 Lean 形式化任务，从人工认领变成 AI 快速交付。
- 瓶颈换了位置：长证明容易生成，短而可消化的证明仍然难。
- AI 会局部精简，不会全局重构：AI 能按提示压缩代码，但很难主动发现可抽象的通用引理。
- 数学家的活，变成搭证明工程：人类更像证明系统的架构师，要先设计 scope、接口和抽象层次。
本期图内信息均按「原文称 / 陶哲轩称 / IPAM 项目页显示」口径整理；没有把 AI 自动形式化解读成已能独立完成数学研究。
评论
登录后可发表评论。