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

> 原标题：当陶哲轩说AI跨过了数学形式化的临界点

- 来源：Computing Life · Share · 鸭哥调研
- 发布时间：2026-06-23T00:00:00.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/40205
- 原文：https://yage.ai/share/tao-lean-formalization-credibility-20260623.html

## 摘要

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

## 推荐理由

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

## 锐评

陶哲轩这次报告的拐点，得分两层看。第一层是AI生成的证明被Lean这个“数学批改器”确认无误，以前需要既懂数论又会形式化语言的志愿者花几周做的活，现在几小时搞定。在一个门槛极高、公认要靠专业人类的环节上，这确实是实打实的突破。第二层是这些证明虽然没错，但代码冗余、抽象层级选得不对，人拿去读和整理反而成了新瓶颈。arXiv一篇独立报告也记录了同样的模式：Claude Code的证明通过了Lean校验，专家一看发现AI为了交差走了捷径，还自己造了一堆没必要的定义，让整个系统更难用。

陶哲轩花了三年才走到这个判断。他过去一直说LLM像“过度自信的本科生”，在前沿领域没有现成训练数据的地方就失效。这次是在自己亲手推进的项目里，顶着几十位数学家联署“别信炒作”声明的压力，基于实测数据说出来的话。他报告的临界点是工程化形式化的临界点，不是AI自己能发现新定理。路已经有人铺好了，AI只是从慢走变成了快走。