用 Claude Code 配合 Lean 4 一个周末搞定两个数学

我尝试用 Claude Code 跑了一次极限测试，结果在一个周末的时间里，居然把 exact-arithmetic checking 和 proof assistant 这两个数学领域的开放问题给啃下来了。这种效率在以前纯靠人力推导简直不敢想，最核心的突破点在于把大模型的代码生成能力直接挂载到形式化验证工具上，形成了一个闭环的自动化验证流。

这次实操中我最在意的是如何避免 LLM 在数学证明中常见的“幻觉”问题。如果只是让它写一段证明，那大概率会出 Bug。我的具体链路是：让 Claude Code 编写 Lean 4 代码 → 提交给 Lean 编译器 → 编译器报错 → 将错误信息原路回传给 Claude → 自动修正代码。

在这个过程中，我遇到了一个比较典型的类型不匹配报错，当时 Lean 4 提示：

type mismatch
  expected: Nat
  actual: Int

这种报错如果手动改可能很快，但当证明链条长达几百行时，定位起来非常痛苦。我发现通过在提示词里强制要求模型在每一步推理后添加 show 语句来明确当前状态，能极大地降低这种低级错误的出现频率。

以下是我在部署这个工作流时，为了提高成功率对环境配置的一点小建议：
一、确保 Lean 4 的版本与模型训练数据中的版本尽量一致，否则会产生大量由于语法更新导致的伪报错。
二、不要一次性喂给模型整个证明目标，建议把大问题拆解成若干个 lemma（引理），逐个攻克。
三、在配置 .leanrc 时，适当调高内存限制，防止在处理复杂递归证明时编译器崩溃。

这次尝试让我意识到，数学研究正在从“灵感驱动”转向“实验驱动”。只要能构建一套可靠的反馈循环，很多以前觉得需要几个月才能验证的猜想，现在可能只需要一个周末的算力和正确的 Prompt 编排。