陶哲轩第三次翻车后终于成功，顶尖数学家正在被AI编程重新定义

7月11日，菲尔兹奖得主陶哲轩发了一篇博客。他在里面详细记录了自己用AI编程Agent，把24个27年前写的Java数学小程序搬到网页上的全过程。

这篇博客在Hacker News上挂了整整两天。评论区最热门的一条回复是："连Terry Tao都在vibe coding了，我们还有什么理由不学？"

但这个反应恰恰错过了陶哲轩想说的重点。他不是在展示AI有多好用，而是在展示一个更残酷的事实——连他都会翻车，而且翻了三次。

45分钟烧光Token，电脑直接崩了

陶哲轩这次任务的目标听起来很朴素：把一个叫"单例定律"的数学命题，从自然语言变成Lean定理证明器能验证的代码。这个定律本身不复杂——单例集合{x}属于A的条件等价于某些子集属性。但在类型论严苛的Lean系统里完成形式化，要写大量对语法要求极高的代码。

九个月前，他用GitHub Copilot手动完成了同样的证明。这次换成Claude Code重做，想对比两代AI编程工具的代际差距。

第一次尝试，他只给了一句宏观指令："完成整个证明"。Claude Code连续跑了45分钟，烧光了Token配额，电脑崩溃，什么都没产出来。

第二次改了策略，把任务拆细。AI这次跑通了，但生成的代码有逻辑错误——它"证明"了一个数学上不成立的命题。

第三次才成功。陶哲轩在视频里苦笑说："这是第三次尝试了，前两次都翻车了。"

一个Fields奖得主，面对一个基础集合论命题，用了三次才让AI做对。这说明的不是AI有多强，而是AI的"强"和你需要的"对"之间，有一道巨大的鸿沟。

AI替你写的不是代码，是"看起来像代码"的东西

陶哲轩的翻车不是个案，而是一个精确的隐喻。

AI编程工具在2026年的能力已经能让任何外行在26分钟内做出一个完整的App——这件事今年7月刚被一个直播验证过。但如果把镜头拉近，你会发现"能跑"和"能对"是两个世界。

GitHub Copilot生成的代码中，45%存在安全漏洞。Claude Code在SWE-bench上的高分有相当一部分来自"看起来做对了但实际没修好"的假阳性。AI写的3万行代码，注释全是幻觉——这不是夸张，是2026年7月多家研究机构交叉验证的结论。

陶哲轩的翻车之所以值得认真对待，是因为他翻在了"自己能判断对错"的前提下。一个Fields奖得主能看出AI的证明有逻辑错误，但一个普通程序员能看出自己项目里AI生成的那段并发代码有没有竞态条件吗？

能的概率不大。

但真正被他复活的，是1999年放弃的梦

陶哲轩博客的后半段比前半段更有意思。

在搞定了24个老旧Java程序的移植后，他还做了一件事——复活了一个1999年就放弃的项目。那个项目叫"Minkowski空间中的Inkscape"，是一个狭义相对论可视化工具。他当时写Java写到一半，复杂度超出了他一个人能处理的极限，扔下了。

27年后，他用AI编程Agent花了"几个小时"，把它做出来了。

他原话是："a couple hours of vibe coding with an AI agent."

一个Fields奖得主说自己在vibe coding。放在一年前，这话能把整个学术圈气炸。但放在2026年7月，这句话的震撼点已经变了——不是AI能帮一个天才做他做不到的事，而是AI让一个天才终于能做他"理论上会、体力上做不完"的事。

这才是AI编程对学术界的真正冲击。不是替代，是重新定义"能力"的边界。以前你的能力等于"你会写多少代码"。以后你的能力等于"你能判断多少代码的对错"。会写代码的人遍地都是，能判断代码对错的人，涨价才刚刚开始。

不是陶哲轩变弱了，是AI把"写代码"变成了"审代码"

很多人看完陶哲轩的经历，第一反应是"连他都搞不定AI"。这种反应是危险的——它让你以为问题出在AI不够好。

问题不在AI不够好。问题恰恰在于AI太好了。好到你愿意信任它，好到你懒得逐行检查，好到你把"看起来没问题"当成了"确实没问题"。

陶哲轩之所以能在第三次翻车时发现AI的逻辑错误，不是因为他比AI更懂怎么写代码。是因为他比AI更懂"什么是对的"。这种判断力来源于二十多年的数学深耕，不是任何一个Prompt能教会AI的。

但对于普通程序员来说，情况刚好相反。你比AI更懂怎么写代码——至少目前还是。但当AI一笔写出500行，而你只花了30秒扫了一眼变量名是否合理就点了"接受"时，你已经不是在审代码了。你是在给AI盖橡皮图章。

陶哲轩的翻车是一个警告：你越信任AI，就越容易失去判断力。而失去判断力的那个人，恰好是出了问题要负责的人。

学术界正在裂成两半

陶哲轩的博客在学术圈引发的反应比他预想的更分裂。

一派认为这是"学术不端的新形式"——用AI写证明代码，本质上是在外包学术工作。另一派认为这是"工具进化"——用计算器算乘法不算作弊，为什么用AI写形式化证明就算作弊？

但这两派都忽略了一个更根本的问题：当AI能替代学术工作中最痛苦、最耗时的那部分"繁文缛节"时，留下来给人类做的那部分，恰好是最需要天赋的。

以前一个数学PhD需要两年时间把一个定理完整形式化到Lean里。如果AI能把这件事压缩到两周，那博士生的培养周期要不要变？导师和学生的分工要不要变？整个学术评价体系要不要变？

没有人在讨论这些问题。大家在争AI写的代码能不能算学术成果，但真正该争的是——当AI消灭了学术苦力活之后，"学术能力"的定义是什么。

如果"证明一个定理"不再需要一年，那博士论文的评审标准还应该是"你证明了几个定理"吗？

陶哲轩的经历揭示了一个正在加速的趋势：对于顶尖人才来说，AI编程不是在替代他们的技能，而是在把他们从"制造者"升级为"质检员"。

写代码的时间从几天变成了几小时，但审代码的时间从几分钟变成了几个小时。总时间可能没变，但时间花的节点完全不一样了。

过去你的能力体现在"你能产出多少"。现在你的能力体现在"你能拦截多少错误"。

这听起来像是退步，实际上是升级。制造是体力活，质检是判断力。体力可以训练，判断力需要深度。深度来自于你真正理解这个东西为什么对、为什么错、为什么"看起来对但实际上是错的"。

陶哲轩翻了三次车才让AI做对一个基础证明。但三次翻车之后，他得到了一个可以反复使用的AI工作流。

这才是真正的护城河。不是用AI写代码的能力，是AI写错了你能看出来的能力。