用Claude Code在Lean中形式化证明：AI与定理证明器的协作实践

这次我们来看一个很特别的组合陶哲轩公开演示了用 Claude Code 在 Lean 中形式化证明。很多人第一反应是“数学家也开始用 AI 编程工具了”但更准确地说这个演示展示了 AI 编程 Agent 和一个严格的证明助手之间是怎么协作的Claude Code 负责生成策略、修改代码、读报错Lean 负责把每一步推理都变成机器可校验的形式化步骤。最终得到的不是一个“感觉对”的证明而是一个被证明器接受的证明。如果平时只关注传统的 Python/JS 代码生成可能低估了这个工作流的价值。普通代码编译通过只能说明语法和类型没问题不代表逻辑正确但 Lean 里一个定理被#check接受意味着整个证明链路的每一步都经过了底层逻辑规则的验证。把 Claude Code 放进这个流程里等于给证明工作加了一个“能自动写草稿、还能自己看报错改错”的助手。先说结论这个方向不是概念演示而是可以独立搭建的工作流。本文会带读者完成环境准备、安装和启动 Claude Code、用 Lean 4 创建一个最小证明项目、让 Claude Code 补全证明、故意制造报错再让它修复、最后用非交互模式和批量脚本处理多个证明文件。读完就能判断这件事适不适合自己的数学或研究工作并直接上手试。这篇文章面向的读者有三类正在接触 Lean/Mathlib 的形式化爱好者最近在折腾 Claude Code 安装、配置和第三方模型接入的开发者和研究者以及想了解 AI 工具在科研场景里到底能做到哪一步的人。下面不聊概念直接按“能跑通、能验证、能排查”的顺序写。1. 核心能力速览先把这组合工具的关键能力整理成一张表。所有信息来自公开演示和官方工具的基本能力具体参数以本机版本为准。能力项说明项目类型AI 编程 Agent 定理证明助手的工作流组合核心工具Claude CodeAnthropic 出品的终端 AI 编码智能体配合工具Lean 4交互式定理证明器常配合 mathlib4 使用主要功能生成 Lean 证明脚本、解析编译报错、迭代修复、批量化处理多个证明文件支持平台Windows / macOS / Linux主要在终端运行也有 VS Code 插件和桌面版启动方式命令行启动项目内使用自然语言交互也可用非交互式一行命令本地资源占用很低推理在云端 API 完成本地只运行 CLI 和 Lean 编译器显存要求无不依赖本地 GPU这个场景不需要考虑显存型号接口能力CLI 支持非交互式调用可接入脚本、CI 流水线批量任务支持逐文件或逐目录批量处理 Lean 证明文件主要依赖Node.js/npm、Lean 4elan、对应编辑器插件适合场景数学定理形式化、Mathlib 项目开发、论文中机器可验证的证明、教学演示从表格能看出两件事。第一这个组合对硬件几乎没要求普通开发机就能跑因为它不加载大模型权重核心计算发生在 API 侧。第二它强调的不是“生成一段看起来像样的代码”而是“生成一个能通过编译器校验的证明”所以验证闭环是工作流里最重的部分。2. 适用场景与使用边界这个工作流适合谁三类人最值得尝试。一是做数学形式化研究的人。Lean 社区大规模推进 mathlib4 的过程中很多证明又长又机械Claude Code 这类 AI Agent 可以补全局部策略、修掉编译错误把人类从重复劳动中解放出来。二是研究 AI 辅助数学的人。陶哲轩这个演示本身就是一个公开案例说明通用编程 Agent 可以不经过专门微调就理解 Lean 的语法和策略这对评估大模型在数学推理上的能力很有参考价值。三是想提高代码可靠性的工程师。虽然 Lean 不是主流业务语言但“AI 写代码机器做验证”的循环逻辑和写正式规约、做强类型检查的思路是相通的。边界也要说清楚。Claude Code 不是“自动解题机”它不会凭空把一个大定理变成 Lean 证明它更像是“能干的实习生”需要人类给出定理声明、拆解证明思路它负责把策略填进去并处理编译失败。如果目标问题和现有 Mathlib 库差距很大AI 也会频繁给出残缺证明或错误策略。更关键的是Lean 检查通过只代表逻辑严格不代表证明方向一定符合论文的表达意图最终核验仍然要人来做。使用上的合规和版权边界集中在研究诚信和数据处理上。如果使用 AI 辅助证明并准备投稿、发布预印本或向 Mathlib 提交贡献应当遵守目标平台和期刊的 AI 使用政策在致谢或 README 中注明使用了 AI 工具。另外Lean 项目如果包含未公开的研究材料或私有代码库不要整体上传到云端 API先脱敏或者选择经授权的企业版或私有化部署方案。第三方兼容 API 还需要检查服务商的数据使用条款确认输入数据不会被用于训练或留存。3. 环境准备与前置条件这个工作流的环境准备分三层运行 Claude Code 的 Node.js 环境、Lean 4 编译环境、编辑器集成。这里按通用流程写不锁死具体版本号。3.1 Node.js 与 npm 环境Claude Code 官方主推 npm 全局安装所以 Node.js 和 npm 是必须先装的。安装版本建议按 Claude Code 官方文档标记的受支持版本选择一般常见的 Node.js LTS 版本都能用。安装完成后在终端确认node --version npm --version如果之前没装过 npm或者遇到权限问题优先用 nvm 管理 Node 版本避免全局目录权限纠纷。3.2 Lean 4 与 elan 工具链Lean 4 的推荐安装方式是使用 elan它是 Lean 的版本管理工具类似于 Rust 的 rustup。安装命令curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh安装完成后新开的终端窗口里确认命令可用lean --version lake --versionlake是 Lean 的项目管理和构建工具相当于 Lean 世界的包管理器和构建器。后续新建项目、拉取 mathlib4 依赖、编译验证证明都会用到 lake。3.3 编辑器插件VS Code 是 Lean 社区最常用的编辑器。在扩展市场安装官方 Lean4 扩展扩展 ID 是leanprover.lean4。安装完成后打开一个 Lean 文件插件会实时显示每个目标的状态、已用假设和当前错误信息。这一步极其重要因为后面让 Claude Code “看报错”时它处理的本质上就是 VS Code 中 Lean 插件会显示的那一类诊断信息。如果不用 VS Code也可以用 Lean 官方支持的其他编辑器插件但本文按 VS Code 展开。3.4 创建 Lean 项目不建议直接裸写 .lean 文件正式做形式化建议先用 lake 初始化项目lake new demo cd demo然后在lakefile.lean中声明 mathlib4 依赖。由于 mathlib4 本身很大第一次执行lake update和构建会拉取大量依赖耗时较长建议在网络状况稳定的环境下执行。也可以先从不需要 mathlib 的简单 Lean 定理开始验证流程后续再加载完整依赖。4. Claude Code 安装部署与启动方式4.1 全局安装 Claude Code确认 Node.js 就绪后安装 Claude Codenpm install -g anthropic-ai/claude-code安装后先确认版本claude --version如果提示claude: command not found或failed to run claude code: error: could not locate the claude cli on path通常是 npm 全局 bin 目录不在 PATH 里。排查方式和完整方案在第 8 章。4.2 登录与认证首次运行claude会进入登录流程。按终端提示完成认证后Claude Code 会在本机保存凭证。如果后续要切换账号或重新认证可以在交互会话里使用对应的账号命令处理。没有 Anthropic 官方账户访问渠道的读者可以使用服务商提供的 Anthropic 兼容 API 端点。这种做法不对应任何特殊网络操作只是把 API Base URL 和密钥指向经授权的第三方服务。常见做法是通过环境变量设置export ANTHROPIC_BASE_URLhttps://api.example.com/v1 export ANTHROPIC_AUTH_TOKEN你的API Key设置完成后再次运行claude。不同服务商的环境变量名可能略有差异以服务方文档为准。这里要特别注意如果 Base URL 指到了不支持某个模型名的端点或者配置里填的模型 ID 在服务商那根本不存在就会触发类似deepseek-v4-pro is not a model this version of claude code recognizes的报错第 8 章会专门排查。4.3 在 Lean 项目目录中启动进入 Lean 项目根目录然后启动cd ~/path/to/demo claude启动后Claude Code 默认会读取项目里的CLAUDE.md文件作为项目说明。建议在 Lean 项目根目录放一份CLAUDE.md写清楚项目用的 Lean 版本、依赖工具、证明风格以及遇到编译错误时应该先看哪类输出。例如# Lean 项目说明 - Lean 版本Lean 4具体版本见 lean-toolchain 文件 - 构建命令lake build - 文件位置证明文件放在 Proofs 目录 - 工作方式每次修改 .lean 文件后先运行 lake build 确认证明通过再向用户汇报这样每次会话 Claude Code 都有足够的上下文不必反复复述项目信息。这个文件对批量任务尤其有用。4.4 在 VS Code 中配合使用如果安装了 Claude Code 的 VS Code 扩展或桌面版可以直接在编辑器里选中代码片段让 Claude Code 对当前文件做修改。操作逻辑和在终端里几乎一样区别只在交互入口。实际工作中建议 Lean4 插件负责显示证明状态Claude Code 负责把报错翻译成可执行的修复动作两边侧重点不同但配合很顺。5. 功能测试与效果验证这一章用一个最小 Lean 项目演示完整闭环。注意下面的例子是通用 Lean 入门素材用来验证工作流不代表陶哲轩原始演示中的具体定理。5.1 测试一个简单定理在项目里新建一个文件Proofs/Demo.lean内容先写成带sorry的占位形式。sorry在 Lean 里表示“暂时跳过证明”正式提交给 mathlib 前必须清掉但用来给 Claude Code 当任务入口很方便。import Mathlib theorem add_comm_demo (a b : ℕ) : a b b a : by sorry在 Claude Code 交互会话中输入自然语言指令请补全 Proofs/Demo.lean 中 add_comm_demo 的证明。完成后运行 lake build确认没有报错后再回复我。Claude Code 会修改文件、尝试不同的 tactic、循环查看编译输出直到lake build通过。最后文件可能被改成类似下面这样import Mathlib theorem add_comm_demo (a b : ℕ) : a b b a : by induction a with | zero simp | succ a ih simp [ih]判断成功的标准很简单lake build无报错如果使用 VS Code Lean4 插件编辑器右下角或诊断面板里没有任何错误标记。同时可以看 Claude Code 是否会解释自己为什么选择induction而不是rw这一步能帮助判断 AI 是真正理解了目标结构还是在碰运气。如果它只给出了最终代码却没有解释可以追问一句“为什么这一步可以用 induction 展开 a”。5.2 故意制造报错测试迭代修复能力Claude Code 的价值在于错误恢复。把证明故意改错让它读取文件再修复import Mathlib theorem add_comm_broken (a b : ℕ) : a b b a : by rw [Nat.add_comm]这个例子里的rw用法与目标结构不匹配Lean 会给出类型不匹配或无法重写的诊断。把如下指令发给 Claude CodeProofs/Demo.lean 目前编译不通过请查看报错信息修复 add_comm_broken 的证明确保