企业官网建设流程全解析

“陶哲轩也在用 Claude Code 做形式化证明”——这则消息在数学和 AI 圈子里传开后，很多人都开始重新审视 AI 辅助数学研究的边界。以往我们认为，形式化证明是门槛极高的硬核技能：要懂定理证明器、要熟悉形式化数学库、要掌握大量战术命令。而现在，Claude Code 这类 AI 编程代理，正在把这件事变成“用自然语言描述证明思路，AI 帮你补全、迭代、修错”的高效工作流。

本文会围绕这条主线展开三块内容：

• 什么是形式化证明，Lean 为什么是当前最值得投入的证明助手；
• 如何在本地从零搭好 Claude Code + Lean 环境；
• 用 Claude Code 辅助在 Lean 中完成一个真实证明的完整实战，包括代码、命令、排错和工程建议。

无论你是数学专业的学生、对 Lean 好奇的开发者，还是想探索 AI 辅助科研的工具党，这篇文章都能帮你把这条路走通。

1. 背景与核心概念

1.1 形式化证明是什么

形式化证明，简单说就是把数学证明写成计算机可验证的、逐字逐句精确的推导步骤。传统论文里的证明，经常会有“显然”“同理可得”“细节留给读者”这类描述，人脑能理解，但计算机无法执行验证。形式化证明要求每个推理步骤都落到一套严格定义的逻辑规则上，最终由计算机确认定理成立。

为什么要做形式化证明？因为它能做到人类力所能及的严谨：

• 避免“微妙的证明漏洞”；
• 让复杂定理可以在不同项目中被复用；
• 特别适合协同工作——多人同时往一个数学库贡献证明，互不干扰，可靠性高。

缺点也很明显：学习成本高。传统数学学习是“定义—直觉—证明”，形式化证明则多了一层“机器语言翻译”，过去很多数学家被这层翻译过程劝退。

1.2 Lean 是什么

Lean 是由微软研究院推出的交互式定理证明器，目前主流版本是 Lean 4。它有几个关键特性：

• 它同时是编程语言和证明语言；
• 编写证明时，证明本身也是一段能被类型检查器验证的代码；
• 围绕 Lean 的社区数学库 mathlib 非常庞大，覆盖了大量现代数学内容。

在 Lean 里写证明，通常有两种风格：

• term 模式：直接提供证明项，偏函数式编程；
• tactic 模式：像和证明器“对话”，通过一系列战术命令逐步推进目标，更贴近人类解题直觉。

绝大多数实际项目用的是 tactic 模式，因为可读性和迭代效率更高。

1.3 Claude Code 在其中的位置

Claude Code 是 Anthropic 推出的终端 AI 编程代理，可以在命令行中读取项目文件、生成代码、执行命令、根据报错迭代修复。它不仅能写日常业务代码，也能处理 Lean 项目中的.lean文件。

在形式化证明流程中，Claude Code 的典型作用是：

1. 根据自然语言描述的定理，生成 Lean 代码骨架；
2. 面对 Lean 编译报错，自动分析原因并修改证明；
3. 搜索 mathlib 中已有的引理，减少手动查库的负担；
4. 把一段不完整的证明补完。

它不能替代数学家想清楚“证明的主线思路”，但它能极大压缩“表达为形式化语言”的摩擦成本。这正是陶哲轩这类数学家愿意尝试它的核心原因——AI 把机器翻译环节的负担接过去了。

1.4 本文的实践目标

为了不让概念停在纸面上，我们会在后面的章节完成一个完整示例：在 Lean 中形式化证明一个简单的数学命题，并使用 Claude Code 来辅助完成代码编写与错误修复。

示例命题：

对任意自然数 a、b、c，有 a + (b + c) = (a + b) + c。

也就是自然数加法的结合律。这个命题在 paper 上三行就写完了，但在 Lean 里体现的是完整的“环境和项目组织—代码生成—编译迭代—证明成功”流程，足够让你举一反三。

2. 环境准备与版本说明

在动手之前，先把环境整明白。本文的操作环境以macOS / Linux为主，Windows 用户可以开启 WSL 后按同样步骤操作。

2.1 需要准备的工具

说明一点：Lean 的具体版本号更新很快，不建议死记硬背某个版本，重点是用elan固定项目工具链，保证不同环境下行为一致。版本需要根据你的项目实际情况调整，本文示例以常见环境为例，重点演示配置思路。

2.2 安装 Claude Code

在终端执行：

npm install -g @anthropic-ai/claude-code

安装完成后，在终端执行：

claude --version

如果能看到版本号，说明安装成功。此时运行claude会进入交互式终端，也可以直接执行一次性指令：

claude "请帮我分析当前目录下的 Lean 文件"

Claude Code 执行期间会读取目录文件、生成代码、执行命令，因此建议在项目目录中启动，并且注意权限边界——生产环境上的敏感目录不要随意让它操作。

2.3 安装 Lean 4 与 elan

Lean 4 推荐用elan管理，它是类似rustup的版本管理器，可以按项目自动切换 Lean 版本。

在终端执行：

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

安装完成后，重启终端，验证：

elan --version

如果需要安装固定版本，可以执行：

elan toolchain install stable elan default stable

Lean 4 安装好后，系统会同时提供两条命令：

• lean：Lean 编译器；
• lake：Lean 项目构建工具，负责依赖管理、构建和运行。

2.4 安装 VS Code 扩展

VS Code 是体验最好的 Lean 交互式编辑环境。打开扩展面板，搜索并安装两个扩展：

1. Lean4：官方 Lean 语言支持，提供实时类型检查、错误提示和#check、#eval等交互命令；
2. Claude Code for VS Code（如果已安装或需要 GUI 方式）：用于直接在编辑器内调用 Claude Code，并非必需，但便捷性更高。

安装完后，打开任意.lean文件，Lean 扩展会自动识别项目环境。

2.5 创建 Lean 项目

下面我们创建一个新项目，命名为lean-demo：

lake new lean-demo cd lean-demo

执行后目录结构如下：

lean-demo/ ├── LeanDemo.lean ├── lakefile.toml ├── lean-toolchain └── Main.lean

各文件的含义：

• lean-toolchain：声明项目使用的 Lean 版本；
• lakefile.toml：项目配置文件和依赖声明；
• LeanDemo.lean：项目库入口；
• Main.lean：可执行程序入口，常用于写测试。

为了使用 mathlib 里的基础引理，需要在lakefile.toml中加上 mathlib 依赖：

[[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" rev = "master"

注意：rev = "master"表示跟随 mathlib 最新主分支。如果后续项目需要稳定复现，建议用具体 commit 哈希锁定版本。修改完配置后，在项目目录执行：

lake update

这个命令会拉取依赖。首次拉取 mathlib 时间较长，需要耐心等待。

3. 核心配置与 Lean 语法拆解

在让 Claude Code 帮你写证明之前，先花一点时间理解 Lean 项目中的几个关键概念，否则即使 AI 生成了代码，你也看不懂它在干什么。

3.1 lean-toolchain 文件

lean-toolchain文件内容很简单，例如：

leanprover/lean4:v4.12.0

elan读取这个文件后，会自动选择对应版本的 Lean 工具链。这里不写死具体版本号，以你安装时的稳定版为准。

3.2 导入 mathlib 与 #check 命令

在Main.lean中写：

import Mathlib.Data.Nat.Basic #check Nat.add_assoc

• import导入 mathlib 中的自然数基础模块；
• #check是 Lean 中的“查询命令”，用来查看某个定理、函数或表达式的类型。

如果一切正常，Lean 扩展会在侧边栏或悬停提示中显示：

Nat.add_assoc : ∀ (a b c : ℕ), a + b + c = a + (b + c)

也就是说，mathlib 里已经有加法结合律了。这个例子有助于理解 Lean 中的“定理”本质上就是“一种类型”，证明则是构造这个类型的值。

3.3 定理声明与 tactic 模式

用 Lean 声明一个定理的格式：

theorem theorem_name (参数列表) : 命题 := by -- 战术证明

例如：

theorem my_add_assoc (a b c : ℕ) : a + (b + c) = (a + b) + c := by exact Nat.add_assoc a b c

要点：

• (a b c : ℕ)声明三个自然数变量；
• a + (b + c) = (a + b) + c是要证明的命题；
• by进入 tactic 模式；
• exact Nat.add_assoc a b c表示直接使用 mathlib 中的现成引理，并把参数填上。

3.4 更“笨”的证明方式：递归与 rfl

如果不用现成引理，而是从定义出发证明，可以这样写：

theorem my_add_assoc_v2 (a b c : ℕ) : a + (b + c) = (a + b) + c := by induction a with | zero => simp | succ a ih => simp [Nat.add_assoc, ih]

这里induction是数学归纳法，zero分支处理a = 0的情况，succ a ih分支处理a = n + 1的情况，ih是归纳假设。这个写法虽然简单，但背后对应的是严格的递归定义，理解它有助于理解 Lean 为什么能验证证明。

3.5 Claude Code 如何接入 Lean 项目

Claude Code 的本质是读文件 + 写文件 + 执行命令。它在 Lean 项目中工作流如下：

1. 读取.lean文件内容；
2. 理解文件中的定理声明和目标；
3. 生成证明代码；
4. 在终端执行lake build或lake env lean检查；
5. 根据报错信息迭代修改；
6. 直到通过验证。

因此，你可以直接用自然语言向 Claude Code 下达指令，比如：

claude "在 Main.lean 中证明自然数加法结合律，使用归纳法思路，先运行 lake build 验证"

Claude Code 会自己创建或修改文件，并多次运行构建命令，直到得到“No errors”的结果。

4. 实战：用 Claude Code 在 Lean 中完成形式化证明

接下来是本文的核心章节，我们完整走一遍“Claude Code + Lean 形式化证明”的实战。

4.1 创建项目结构

在项目目录lean-demo中，先把测试文件准备好。在Main.lean中写入：

import Mathlib.Data.Nat.Basic -- 声明一个待证明的定理 theorem demo_add_assoc (a b c : ℕ) : a + (b + c) = (a + b) + c := by -- TODO: 完成证明 sorry

这里故意留下sorry，表示“暂时跳过证明”。sorry在 Lean 中会让编译通过，但会产生警告，它不是正式证明，只是占位符。

接下来我们用 Claude Code 来完成证明。

4.2 向 Claude Code 发出指令

在lean-demo目录下运行：

claude "请查看当前目录，读取 Main.lean，这个文件里有一个未完成的定理 demo_add_assoc。请完成该证明，不要使用 sorry，并运行 lake build 验证结果。"

Claude Code 的执行过程大致如下：

• 读取文件，识别demo_add_assoc；
• 判断需要证明的命题是加法结合律；
• 搜索可用的 mathlib 引理；
• 生成exact Nat.add_assoc a b c或归纳法证明；
• 写入文件；
• 执行lake build；
• 检查是否报错。

最终文件内容可能类似：

import Mathlib.Data.Nat.Basic -- 声明一个待证明的定理 theorem demo_add_assoc (a b c : ℕ) : a + (b + c) = (a + b) + c := by induction a with | zero => simp | succ a ih => rw [Nat.add_succ, Nat.add_succ, ih]

4.3 人工理解 Claude Code 生成的证明

上面生成的证明，我们一行一行拆解：

1. induction a with：对a做数学归纳。
2. | zero => simp：当a = 0时，0 + (b + c)和0 + b + c都化简为b + c，simp直接完成。
3. | succ a ih =>：归纳步骤，假设命题对a成立，其中ih就是归纳假设：

   ih : a + (b + c) = a + b + c

4. rw [Nat.add_succ, Nat.add_succ, ih]：利用Nat.add_succ把(a+1) + ...展开，然后用ih替换，最终消掉目标。

这种证明是 Lean 中最常见的“定义展开 + 归纳假设”套路。

4.4 运行与验证

在终端执行：

lake build

如果一切正常，输出中不会出现 error。Lean 4 编译成功时通常不打印额外信息，退出码为 0。

也可以直接在 VS Code 中打开Main.lean，把光标放在证明结尾处，如果没有任何红色波浪线，说明证明通过。

为了进一步验证，可以添加一行#check demo_add_assoc：

#check demo_add_assoc

Lean 扩展会显示：

demo_add_assoc : ∀ (a b c : ℕ), a + (b + c) = a + (b + c)

当然这里显示的是最终定理的类型签名。

4.5 让 Claude Code 做更深的事情

以上只是最基础的应用。在实际项目中，Claude Code 还可以完成这些更复杂的辅助工作：

• 搜索 mathlib 引理：当你不确定某个引理是否已存在时，可以让 Claude Code 运行#check或#find查找；
• 分析错误信息：Lean 的报错有时很紧凑，Claude Code 可以根据错误自动修改证明策略；
• 批量补全多个定理：如果一个文件里有多个sorry，可以让 Claude Code 逐个完成；
• 改写证明风格：让它在“简洁的 tactic 风格”和“可读性更高的逐步展开风格”之间切换。

例如，你可以继续下指令：

claude "请把 demo_add_assoc 的证明改成 term 模式，使用 exact Nat.add_assoc a b c"

Claude Code 会重写文件，然后重新验证。

5. 常见问题与排查思路

在实际操作中，环境搭建和 AI 辅助生成的环节都可能遇到问题。下面按问题现象、常见原因、解决思路来梳理。

5.1 关于模型配置的高频问题

很多用户会通过配置文件指定第三方模型或自定义 base URL。常见的做法是在 Claude Code 的配置中添加 model 相关设置，但有一点非常重要：

模型名称必须严格匹配当前 Claude Code 版本支持的接口名。不同版本支持的模型集合不同，升级 Claude Code 后可能出现模型不识别。

遇到类似报错时，先升级工具本身，然后确认模型名是否拼写正确，最后检查配置文件是否有残留的旧版设置项。

5.2 安全与授权提醒

Claude Code 会在你的授权下执行终端命令。使用它操作重要代码库、数据库或生产环境时，务必注意：

• 在测试分支或独立目录中运行；
• 明确授权范围，不要让它无限制执行删除或覆盖命令；
• 涉及关键变更前先提交当前版本，保留回滚点。

这不是小题大做。AI 代理的执行效率越高，潜在破坏力也越大，养成良好的工程习惯比依赖 AI 的“聪明”更重要。

6. 最佳实践与工程建议

有了环境、跑通了一个小证明，还要把这项能力真正沉淀成可复用的工程流程。下面几条建议来自实际摸索。

6.1 从简单引理起步，形成“证明—校验”闭环

不要一开始就让 Claude Code 去证明一个前沿数学定理。建议从 mathlib 中已经成立的简单引理开始，让 AI 尝试证明，并强制它跑完lake build。

这个过程的目的不是证明本身，而是让 AI 和你的项目形成“错误反馈”闭环。AI 能意识到哪些报错会导致失败，你也能逐渐看懂 Lean 的战术输出。

6.2 把自然语言思路先写进注释

在.lean文件中，先用中文或英文注释写出证明思路：

-- 对 a 做数学归纳。 -- 基础情况：a = 0 时两边化简为 b + c。 -- 归纳步骤：利用 a + (b + c) = a + b + c 的归纳假设。 theorem demo_add_assoc (a b c : ℕ) : a + (b + c) = (a + b) + c := by induction a with | zero => simp | succ a ih => rw [Nat.add_succ, Nat.add_succ, ih]

Claude Code 对注释很强的理解能力。注释本身就是给 AI 的提示词，能显著提高生成代码的准确率。

6.3 使用版本锁定保证可复现

数学形式化项目往往有较长的生命周期。在lakefile.toml中：

• 尽量使用固定的 commit 哈希而不是master；
• 记录 Lean 工具链版本；
• 把关键依赖的版本信息写进 README。

这样换一台机器、换一个时间点，项目还能稳定编译。

6.4 区分“探索”与“沉淀”

用 Claude Code 做形式化证明时，会有两种工作模式：

• 探索模式：让 AI 自由尝试多种证明路径，快速看哪些可行；
• 沉淀模式：把验证通过的证明整理成结构清晰、可读性高的最终版本。

探索时可以写临时文件；沉淀时务必把证明格式化、加注释、拆函数。不要让“AI 能打印出可运行代码”变成“项目代码不可维护”的借口。

6.5 理解 AI 辅助证明的局限

聊了这么多 Claude Code 的优势，也要说说它的边界：

• 它不能代替数学直觉：证明的关键步骤仍需要人来设计；
• 它对上下文有限制：超大项目、超长的证明过程可能需要拆分成多个会话；
• 它会犯错：AI 生成的证明可能不是最优的，甚至可能是错的，但 Lean 会兜底——编译不通过就是假的。

这也是形式化证明最妙的一点：AI 可以大胆尝试，机器严格把关，数学家专注策略。人、AI、证明器三方配合，构成了一条全新的数学工作链。

6.6 推荐的学习路线

如果你从零开始，建议按下面顺序推进：

1. 学会 Lean 基础语法，理解theorem、by、rw、simp、exact；
2. 完成 5 到 10 个简单自然数命题的证明；
3. 用 Claude Code 辅助完成中间难度的证明；
4. 阅读 mathlib 中真实定理的证明源码，学习优秀的证明风格；
5. 尝试把你的数学笔记中一个小定理形式化；
6. 参与开源数学库的贡献，把经验沉淀到社区。

形式化证明不会替代传统数学，但它会成为数学研究的重要基础工具。Claude Code 这类 AI 代理的价值，则是把这条路的入门门槛再一次降低。

7. 总结

回到开头的问题：陶哲轩使用 Claude Code 在 Lean 中做形式化证明，为什么引发这么大的关注？因为这件事背后是一种新范式的雏形——数学家不再需要事无巨细地掌握证明器的所有细节，而是把“想法翻译成机器语言”的任务交给 AI。

本文完整梳理了从环境搭建到 Lean 证明实战的整套流程，包括：

• Claude Code 的安装与项目接入；
• Lean 4、elan、lake、VS Code 的环境配置；
• 自然数加法结合律的完整证明示例；
• 常见报错的排查思路；
• 把 AI 辅助形式化证明纳入工程化工作流的建议。

如果此刻你手边正好有终端，不妨照着创建一个 Lean 项目，写下一句证明目标，然后把剩下的工作交给 Claude Code 试试。你可能会发现，形式化证明这座曾经看起来很高的山，走过去后回望，其实有了一条 AI 铺好的小路。