2026/6/22 · 18:24
AI 证明太快了
量子位新文图片笔记：陶哲轩在 IEANTN 项目中观察到 AI 已把部分形式化证明任务从数周缩到数小时，新的难题变成人类如何审查、消化和重构证明。
ギャラリー
这张图片笔记压缩自量子位新文：陶哲轩在 IEANTN 项目中发现，AI 已把部分数学形式化任务从「志愿者等数周认领」推进到「数小时完成」，但新的瓶颈变成了人类如何审查、精简和重构这些证明。1
图里保留了 3 个关键信号：
- IEANTN 试图把显式解析数论中的技术性论文形式化，在 Lean 中建立可动态更新的数论估计网络；量子位文中转述，繁琐的数值验证和参数匹配占陶哲轩解析数论思考时间至少 70%。1
- AI 可以快速交付局部形式化证明，甚至让项目里待认领的未解决 issue 队列基本清空；这把等待时间从数周压到数小时。1
- 问题转向「证明消化」：AI 证明常有数百行冗余，能做局部 code golf，却不能自发发现更高层次的全局重构机会。1
一句话：数学家的角色正在从亲手做每块证明，转向设计任务边界、接口和抽象层次，让 AI 交回来的拼图能拼进整体蓝图。1
コメント
ログインするとコメントできます。