新智元报道
全球知名数学家陶哲轩亲身经历了一场与AI的较量，他的实验警告人们：技术越先进，人类就越不能放松警惕。
在一次长达45分钟的操作后，电脑因过度计算而直接死机了。
世界顶尖数学家陶哲轩在测试一种最新的AI编程工具时遇到了一个令人惊讶的问题。
几个月前，他在视频中展示了如何将复杂的数学证明进行形式化处理。
然而在九个月后，面对备受推崇的新一代AI助手Claude Code，他原本以为这会是一次轻松的胜利。
未曾料到的是，在第一次全权委托给AI时，不仅没有得到预期的结果，还导致了电脑崩溃。
在收到一个宏大的指令之后，AI陷入了无休止的尝试和错误循环中，结果不仅未能生成任何可用代码，反而使系统过载直至死机。
当前科技圈热议的话题是关于智能体的能力边界。
似乎只要给出一句简单的指示，AI就能替你完成所有任务。然而陶哲轩的实际测试证明了这种想法过于理想化：
即便面对最先进的技术，人类也必须保持清醒的头脑和积极的参与。
持续的人类介入才是最有效的使用方式。
「一波流」幻想破灭
AI助手可能遇到的过载问题
故事回到几个月前。
在Equations of Theories项目中，陶哲轩利用GitHub Copilot和conical工具，通过人类智慧与轻度AI辅助完成了复杂证明的形式化工作。
如今，新一代智能体已经登场。
由于对新技术的过度信任，陶哲轩在初次尝试Claude时步入了常见的误区，即给它下达一个过于宽泛的任务：「请完成所有事项。」
他原本以为AI会自动分解任务并输出完美的代码。
然而这样的指令直接触发了机器的过载陷阱，在面对复杂逻辑链时迷失方向。
它在尝试各种可能的方式后，错误不断积累，导致长时间反复推倒重来。
在消耗大量计算资源之后，AI依旧未能完成任务，并且陶哲轩的电脑也因此崩溃。
实践证明，如果给AI下达的任务指令缺乏明确界限，它的努力反而会像无头苍蝇一般四处乱撞，最终导致无效的资源浪费。
这次失败的经历揭示了一个重要的事实：认为有了智能体就可以完全依赖它而不用参与的想法是不切实际的。
「保姆级」指令的胜利
转机出现在第二次和第三次尝试中。
第二次尝试已经取得了成功。
陶哲轩将任务拆解成多个小部分，不再要求Claude一次完成整个证明。他先形式化引理1、引理2和引理3，然后逐步补充完整证明。
最终在大约25分钟内完成了完整的证明。
在第三次尝试中，他还探索出了一套防止AI失控的策略，核心在于将所有指令详细记录在一个Markdown文件里再交给Claude执行。
这种做法的精髓在于控制和简明性。
第一步是先确立符号系统，然后再逐步推进证明过程。
在第二步中，他创建了一个初步的证明框架，并在这一阶段使用「sorry」占位符来避免AI陷入细节上的反复尝试。
这个策略背后的思想在于：防止让AI过早进入试图解决所有问题的状态。
与其让它一上来就全力冲刺，不如先搭建好基本结构再慢慢完善。
接下来的任务是将非形式化的证明逐行转换成Lean代码，并继续使用「sorry」来避免不必要的复杂化。
这个过程像盖房子一样：先立起梁柱再砌墙，而非一开始就试图完成所有工作。
陶哲轩还发现Claude的一个有趣弱点：它在处理机械性任务时反而容易变得过于繁琐和复杂。
人类可能会觉得这些步骤一目了然，而AI却倾向于采用更复杂的途径来解决。
这正是许多人误解AI的地方所在。
认为它擅长细小的工作，但实际上在需要执行具体任务时往往会过于自由发挥。
在形式化证明中，过度的创新反而可能成为问题的根本原因。
遵循详细的指令步骤后，Claude最终能够老实地按照人类设定的方向推进工作，并迅速生成了正确的代码框架。
你填空我修Bug
这次实践中最令人印象深刻的部分是人机之间的流畅合作。
在进展过程中电脑再次崩溃了一次。
然而这次，由于任务已经被拆解为小部分步骤，恢复起来相对简单得多。
「人机并行协作」
将工作分解成小块不仅防止了AI失控，还让后期修改变得更加容易。
更具亮点的是在调试阶段的表现。
在填充细节时，Claude遇到了一个底层逻辑问题。陶哲轩发现它错误地两次展开了一个简写表达式SA，而实际只需要一次即可。
面对这样的死胡同时，AI试图通过复杂的路径绕过障碍，甚至提供了冗长的代码。
此时人类的作用显现出来。
陶哲轩迅速接管这一逻辑部分，并利用Info View面板解决了问题。他使用了congruence命令消除了多余项，使错误信息瞬间消失。
接着他还意识到可以将H1提取为一个关键方程引理以供后续重复使用。
此刻，真正的协作编程场景上演了。
当陶哲轩在处理复杂的逻辑修复时，Claude Code并未闲着。
它默默地调整代码结构，并自动将H1替换成了简洁的证明形式，还为后续引理搭好了框架。
这种情况下，AI不仅遵循指令执行任务，还能自主优化代码并提前准备后续步骤。
在人机协作的最佳状态下，双方在同一个代码库中独立运作却又能默契配合。
这次实验耗时大约半小时，其中包括一次系统崩溃。对比之前45分钟的空转和电脑死机的情况，这次的结果显然更加高效。
陶哲轩通过此次试验得出了一种非常现实的技术态度：必须坚持参与其中并不断调整策略以达到最佳效果。
尽管Claude Code足够强大，大多数人可能会认为让它全权负责会更省心。
然而一旦这样做，它很可能抛弃原有的高效思路，按自己的方式重新编写代码。
这种做法可能导致生成的代码难以理解且调试困难。
此外，他还指出同时使用多个智能体并用另一个来管理的做法未必有效，至少在此次任务中他更倾向于单个可控的Agent。
拒绝「多智能体焦虑」
要把手放在方向盘上
在技术快速发展的背景下，人类必须保持参与感以确保工作效率和质量。
最佳的工作方式不是完全依赖工具，而是始终掌控局面。
因为一旦过度依赖，出现问题时往往只能重新开始或求助于黑箱式的解决方案。
相反地，当坚持「人在回路」的原则，你就能更好地利用AI的潜力来解决问题。真正指挥剑的方向的人依然是人类自己。
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