陶哲轩亲测Claude跑崩电脑，全靠这份保姆级指令清单翻盘

sinalook

陶哲轩亲测Claude跑崩电脑，全靠这份保姆级指令清单翻盘

菲尔兹奖得主陶哲轩分享了使用 Claude Code 完成 Lean 数学形式化证明的实测经历，为 AI 工具的高效使用提供了实用参考。其核心任务是将 “单例定律” 的非形式化证明转化为 Lean 可验证代码，这也是他九个月前手动完成过的工作。

首次尝试时，陶哲轩仅下达 “完成整个证明” 的笼统指令，导致 Claude 陷入无意义回溯试错，连续运行 45 分钟后耗尽 Token，还造成电脑崩溃，未产出有效结果。

后续调整策略后，他将任务拆解为符号定义、搭建证明骨架、逐行转化代码等步骤，用 “sorry” 占位符先确立框架再填补细节，仅用半小时便完成证明，期间虽遇电脑宕机，但因分步推进未丢失进度。

实测中发现，Claude Code 存在底层步骤 “过度思考” 的问题，会不必要地展开式子导致逻辑冗余，需人类手动介入简化。现阶段单智能体受控协作已能满足需求，多智能体叠加可能增加复杂度。这一实践表明，AI 在复杂任务中仍需人类明确引导与关键干预，“人类在环” 的协作模式才是当前最优解。