陶哲轩说 AI 跨过了数学形式化的临界点，但可读性成了新瓶颈

当陶哲轩说AI跨过了数学形式化的临界点

陶哲轩在 IEANTN 项目里发现，以前需要懂数论又会 Lean 的志愿者花几周做的形式化任务，现在 AI 几小时就能完成，而且 Lean 这个“数学批改器”确认证明没错。但他同时指出，AI 生成的证明比人写的长几百行，代码冗余，抽象层级选得不对，人去读和整理反而更费劲。他说的临界点只跨过了“证明正确”这一层，“证明能用”这一层反而更卡了。一篇 arX...

推荐理由：三个独立信源——陶哲轩原帖、同行评估、一篇 arX 报告——不是媒体二传手。文章最大的贡献是把“临界点”拆成两层，K 轴很强。扣分点在于这是一篇个人博客分析，不是一手研究发布，所以重要性给 82 而不是更高。