菲尔兹奖得主陶哲轩分享了使用 Claude Code 完成 Lean 数学形式化证明的实测经历，为 AI 工具的高效使用提供了实用参考。其核心任务是将 “单例定律” 的非形式化证明转化为 Lean 可验证代码，这也是他九个月前手动完成过的工作。
首次尝试时，陶哲轩仅下达 “完成整个证明” 的笼统指令，导致 Claude 陷入无意义回溯试错，连续运行 45 分钟后耗尽 Token，还造成电脑崩溃，未产出有效结果。
后续调整策略后，他将任务拆解为符号定义、搭建证明骨架、逐行转化代码等步骤，用 “sorry” 占位符先确立框架再填补细节，仅用半小时便完成证明，期间虽遇电脑宕机，但因分步推进未丢失进度。
实测中发现，Claude Code 存在底层步骤 “过度思考” 的问题，会不必要地展开式子导致逻辑冗余，需人类手动介入简化。现阶段单智能体受控协作已能满足需求，多智能体叠加可能增加复杂度。这一实践表明，AI 在复杂任务中仍需人类明确引导与关键干预，“人类在环” 的协作模式才是当前最优解。