新智元报道

编辑：元宇

【新智元导读】从电脑崩溃到半小时拿下Lean形式化证明，数学大神陶哲轩用亲身踩坑经历警告：AI越强大，人类越不能偷懒，应时刻保持「人类在环」的绝对清醒。

连跑45分钟，烧光Token，最后电脑直接死机。

你可能很难想象，这竟是全球顶尖数学家陶哲轩在实测最新AI编程工具时，遭遇的一次真实翻车现场。

九个月前，他曾在一个视频中向大家展示如何将一段复杂的数学证明形式化。

九个月后，面对被业界疯狂追捧的新一代AI助手Claude Code，他本以为这会是一场降维打击。

没想到，第一次完全放权给AI，不仅没有完成数学证明，还把自己的电脑搞崩溃了。

在接到一句宏大的指令后，AI陷入了疯狂的回溯与试错，狂跑了45分钟，不仅没写出一行可用代码，庞大的计算过载还把电脑弄死机了。

眼下整个科技圈都在狂热地讨论AI智能体。

仿佛只要随手抛出一句话，AI就能替你打理好全部工作。陶哲轩这场硬核实测，却像一剂清醒剂，终结了这种技术幻觉：

即使面对再强大的AI，人类也不能完全「关掉大脑」。

保持参与，才是最好的使用AI的方式。

「一波流」幻想破灭

AI智能体的「过载陷阱」

故事要从九个月前说起。

在当时的Equations of Theories项目里，为了证明等式1689能够推导出等式2（即singleton law），陶哲轩使用GitHub Copilot和一个名叫conical的辅助工具，靠着人类的智慧和轻度的AI辅助，一步步手动完成了证明的形式化。

如今，全面升级的智能体来了。

由于对AI的过度信任，陶哲轩在第一次尝试Claude时进入了一个极其普遍的误区，他给Claude下达了一个大而笼统的指令：「请把整个事情都做完。」

他原本以为，AI会自动拆解任务、理清逻辑、输出完美代码。

然而这句不加限制的指令，直接触发了机器的「过载陷阱」。面对复杂的逻辑链条，Claude在底层引理的证明泥潭里迷失了方向。

它花了大把时间去猜测该怎么做，接着犯错，然后疯狂回溯、推倒重做。

就这样，在烧掉大量Token之后，AI狂跑了整整45分钟仍然一无所获。而且，庞大的计算压力，也让陶哲轩的电脑崩溃了。

事实证明，当人类下达给AI的任务指令缺乏清晰边界时，AI的勤奋只会像无头苍蝇式的乱撞，最终演变成一场徒劳无益的消耗。

这次惨痛的教训，也戳破了当下人们对AI的一个幻觉：认为有了智能体，自己就可以当「甩手掌柜」了。

「保姆级」指令的胜利

真正的转折，发生在第二次和第三次尝试里。

第二次，其实已经成功了。

陶哲轩把任务拆开，不再要求Claude Code一次完成全部证明，而是先形式化引理1、引理2、引理3，再逐步把证明补进去。

最后大约用了25分钟，完整证明做出来了。

在第三次，他还摸索出了一套防AI「暴走」的干货步骤，核心秘诀，就是专门建一个Markdown文件，把所有指令按步骤写清楚，再交给Claude Code执行。

只是这次他并没这么做，而是把这些步骤直接写进Lean文件的注释里。

这套流程的精髓，不在于复杂，而在于克制。

第零步，先形式化S和F这两个记号。先把符号系统立住，别急着证明。

第一步，创建证明骨架。把引理1、引理2、引理3的陈述都形式化出来，但这个阶段严禁AI尝试证明，一律用「sorry」占位。

这一步看似保守，实际上非常高明。因为他已经从第一次失败里看明白了：

一旦让Claude Code过早进入「我要把它证出来」的状态，它就会在证明细节里疯狂打转，反复试、反复错、反复回退，最后什么都做不完。

与其让它一上来就冲刺，不如先让它把结构搭好。

然后才是第二步：把非形式化证明里的每一行，逐行转成Lean代码。

理由先不补，能用「sorry」的地方先用「sorry」。

这个动作特别像搭脚手架。先把房子的梁柱立起来，再慢慢砌墙，而不是抱着一堆砖头就想直接盖完。

也是在这里，陶哲轩点出了Claude Code一个很有意思的弱点：它在最底层、最机械的步骤上，反而容易「想太多」。

本来人类可能觉得「这一步一两行就该结束了」，它却会绕出更长的路径。

在陶哲轩的第一次尝试时，AI甚至不愿意沿用S和F这些简写，而是把式子不断展开，导致证明越来越难读。

这正是很多人今天会误判AI的地方。

你以为它最擅长的是细活，它偏偏会在最该老实执行的时候，突然开始「发挥创造力」。

而在形式化证明这类任务中，过度发挥，往往不是加分项，反而可能是事故源头。

在这套「保姆级」指令的约束下，Claude终于不再像脱缰的野马。它老老实实地跟着人类给定的证明，几秒钟就吐出了规整的代码框架。

「人机并行协作」

你做你的填空，我修我的Bug

真正让这次实践变得好看的，是中间那段非常丝滑的人机配合感。

做到一半，电脑又崩了一次。

但这一次，崩溃没有毁掉进度。

原因很简单：因为任务已经被拆成了一段一段的小步骤，所以恢复起来并不痛苦。

分步推进，不只是为了防止AI暴走，也是为了人类后期修改方便。

更精彩的戏码是在修Bug阶段。

在填补细节时，Claude卡在了某个底层步骤上。陶哲轩发现，AI把记号SA展开了两次，而实际上只需展开一次。

面对这个逻辑死结，AI试图换一种极其复杂的思路去绕过它，甚至给出了一段冗长代码。

这个时候，人类的作用显现了。

陶哲轩果断出手，他调出Info View面板，亲自接管了这行逻辑。

面对多余的展开项，他直接使用congruence（消掉同类项），瞬间清空了报错信息。连他自己都忍不住感慨：「这也太强了，居然直接就成了。」

随后，他又意识到，这里其实可以把H1抽出来，单独作为一个关键方程引理，因为后面两个地方都能复用它。

此时，全场高潮的「人机结对编程」画面出现了。

当陶哲轩在前方手动修复复杂逻辑、提取引理时，Claude Code根本没有闲着。

它在后台默默同步，聪明地把过去代码里的H1替换成了一行简练的证明，并自动给后续的引理三搭好了骨架。

这才是这次实验最舒服的一幕：不是你命令，我执行；也不是你放手，我乱跑；而是两者在同一个代码库里独立运转，互不干扰却又完美配合。

像一场真正的结对编程，只不过你的搭档，不是另一个人类，而是一个需要被约束、但又确实能干活的智能体。

拒绝「多智能体焦虑」

要把手放在方向盘上

最后，这份证明完成了。

总耗时大约半小时，里面还算上了一次系统崩溃。对比第一次45分钟空转到电脑死机，这个结果已经足够说明问题。

但在复盘阶段，这位数学大神给出的，不是某种神话式结论，而是一种很清醒的技术态度。

他显然看到了自动化的诱惑。

Claude Code足够强，大多数人很容易生出一种冲动：干脆让它全包，我少操点心。

可问题在于，一旦你真这么做，它很可能直接扔掉你原本已经很好的非形式化思路，按它自己的方式重写一遍。

结果，就是代码变得晦涩难懂，一旦跑不通，你连调试都无从下手。

他还顺手吐槽了当下很流行的一种趋势：

让多个智能体同时跑，再用另一个智能体去管理前面那几个智能体。

理论上当然可以。

可至少在这次任务里，他已经对单个、听话、受控的Agent非常满意了。再往上叠，不一定是效率提升，也可能只是另一种形式的复杂化焦虑。

此外，在这场技术洪流中，人类必须保持参与感。

最顶级的AI工作流，不是关掉大脑，而是始终把手放在方向盘上。

因为一旦完全依赖工具，出了问题，你能做的往往只剩下一遍遍重新调用，像是在对一个黑箱许愿。

而当你把「人类在环」这件事坚持到底，局面就完全不同了。

这时候，AI不是替你思考的大脑，而是你手里那把越来越锋利的剑。真正决定它往哪儿挥的人，仍然还得是你。

参考资料：

https://mathstodon.xyz/@tao/116190707979654536%20

https://github.com/teorth/analysis/blob/main/analysis/Analysis/Misc/equational.lean%20

https://www.youtube.com/watch?v=JHEO7cplfk8