菲尔兹奖得主陶哲轩，最近干了件让所有程序员和数学家都惊掉下巴的事——他让AI帮他形式化一个数学证明。结果，AI把他电脑弄崩了两次。
是的，你没看错。
那个在YouTube上教了无数人数论的陶哲轩，这次成了AI的“小白鼠”。他要用现在最火的AI编程工具Claude Code，重新做一遍9个月前用GitHub Copilot做过的数学证明形式化。
结果怎么样？
电脑崩了。
这活儿到底多难？
先科普一下什么是“形式化证明”。
简单说，数学家写的证明，就像一篇散文，充满了“显然”“同理可得”这种人类看得懂但计算机看不懂的表述。而形式化，就是把这些模糊的表述翻译成Lean这种证明助手能理解的严格代码。
陶哲轩要形式化的，是方程1689 implies equation two，来自一个叫"equation theories project"的项目。
9个月前，他手动用GitHub Copilot一步步做过一次。那次花了多久？没说，但过程挺痛苦的。
现在有了AI agents，他寻思：这不正好测试一下AI到底几斤几两？
第一次尝试：AI放飞自我
陶哲轩的第一次尝试非常直接。
他就差没说“你给我把整个证明形式化一下”了。
然后AI就“跑飞了”。
整整45分钟，AI在那儿疯狂输出代码，完全停不下来。最后——
电脑崩了。
Token也用光了，证明还没完成。
陶哲轩自己都无语了：“这也算不上成功。”
说实话，这结果意料之中。你让AI一次性干太复杂的活，它就容易“Overthinking”——想太多，做太少。
第二次尝试：分而治之
第二次学聪明了。
陶哲轩把任务拆成了 lemma 1、lemma 2、lemma 3，一个一个来。
果然，25分钟搞定。
但好巧不巧，录制又出了问题，视频没法用。
不过这次他发现了一个关键：给AI好的指令，比啥都重要。
于是他写了份详细的“食谱”，准备第三次实验。
第三次：又崩了，但成了
这就是视频里记录的内容。
这次用的是Claude Code。陶哲轩先把整个任务拆成5步：
- Step 0: 形式化notation
- Step 1: 创建证明骨架
- Step 2: 把每行证明转成Lean代码
- Step 3: 填坑（sorry）
- Step 4: 修修补补
每一步都有详细指令。
效果怎么样？
电脑又崩了。
但这次崩溃是因为——呃，他自己操作失误。
是的，AI没崩，是陶哲轩自己把电脑搞崩的。
后来他换回主电脑，继续让AI干活。这次AI真的把证明形式化完成了，用时大约半小时。
最离谱的发现：AI卡在最简单的步骤上
整个过程中，最让陶哲轩意外的，不是AI不会做，而是AI在最简单的地方卡住了。
比如lemma 1的证明，按理说应该是1-2行代码搞定的事，AI在那儿反复尝试，疯狂消耗token，就像一个学生做不出来题急得满头大汗。
陶哲轩都看乐了：
“It really overthinking it quite a bit.”
而且AI有时候会“自作主张”。如果你把整个任务直接丢给它，它可能会把你给的证明扔到一边，自己搞一套——虽然也能用，但完全对不上你原来的思路。
这就像啥呢？
你让AI帮你写论文，它给你写了一篇全新的，还挺好，但你用不了。
陶哲轩的结论：别想甩手掌柜
那AI到底有没有用？
陶哲轩说：有用，但别全甩给它。
他的策略是：
- 简单重复的活交给AI
- 自己处理关键的、需要理解的步骤
- 保持对整个过程的掌控
“Otherwise, if you rely too much on these tools and something goes wrong, you may have no idea what to do.”
翻译成人话就是：别太懒，该自己动手还得动手。
他还试了试“并行工作”——让AI在后台跑lemma 3，自己同时处理lemma 2。效果还行，但需要很强的多任务能力，一般人可能搞不定。
这事到底意味着什么？
一个菲尔兹奖得主，用最顶尖的AI工具，花半小时才能形式化一个数学证明。
AI确实能干活了，但远没到能“替代人”的程度。
它会崩溃，会overthinking，会自作主张，会在最简单的地方卡住——像极了你我刚学编程时的样子。
但它也确实在进步。
9个月前用GitHub Copilot的时候，过程更痛苦。现在用Claude Code，至少能成了。
也许再过9个月，会更顺利？
或者，也许数学证明的形式化，本质上就是一个需要人机协作的活？
结尾
视频最后，陶哲轩说：
“You can kind of select the level of automation that you're comfortable with.”
这句话挺有意思的。
AI不是来取代谁的，它是来让你选“自动化程度”的。你想躺平，就多交给它；你想自己来，就多动手。
至于选哪个——
反正数学家们暂时还不用失业。
【MiniMax-M2.5锐评】：陶哲轩用半小时证明了一件事——AI离“数学之神”还差得远，但当个“数学工具人”已经勉强及格了。
参考链接：
https://www.youtube.com/watch?v=JHEO7cplfk8