前言

Lean 4 是当前最热门的数学形式化证明语言。随着 AlphaProof 在 IMO 上的表现，越来越多的数学研究者和工程师开始学习 Lean。但 Lean 的学习曲线陡峭，文档分散，踩坑率极高。

我花了 200 个小时学习 Lean，踩了无数坑，写了 5000 行 Lean 代码。这篇文章是我真金白银换来的教训。

坑 1：安装——不要用官方推荐的 elan

症状： 跟着 Lean 官网的"Getting Started"走，用 elan（Lean 版本管理器）安装，结果 VS Code 插件报错、lake 找不到、版本冲突。

根因： elan 本身没问题，但和系统 Python 环境、VS Code 的 Lean 4 插件、已有的 Haskell Stack 等工具链存在隐式冲突。

正确做法：

# 不要用 elan，用 Docker 或 Nix
# 方案一：Docker（推荐新手）
docker run -it leanprover/lean4:latest

# 方案二：Nix（推荐有经验的）
nix-shell -p lean4

# 方案三：如果你坚持用 elan（比如你已经是 Rust 用户）
# 先清理所有冲突工具链
brew uninstall haskell-stack  # 如果有的话
pip uninstall lean  # 如果有 Python lean 包
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

耗时： 我花了 8 小时解决安装问题。如果你按上面做，应该 30 分钟搞定。

坑 2：VS Code 插件——Lean 4 和 Lean 3 插件会打架

症状： 安装了 Lean 4 插件，但语法高亮不工作，info view 空白，或者显示奇怪的错误。

根因： 你可能同时安装了 Lean 3 和 Lean 4 的 VS Code 插件。它们会互相干扰。

解决： 在 VS Code 扩展页面，搜索 “lean”，确保只启用了 “lean4”（发布者是 leanprover），禁用/卸载 “lean”（旧版 Lean 3 插件）。

坑 3：类型类（typeclass）推断——Lean 的"隐形参数"地狱

Lean 的类型类系统是它最强大的特性之一，也是新手最大的困扰。

症状： 写了一个简单的 a + b，Lean 报错：

failed to synthesize instance
  OfNat (Fin n) 0

根因： Lean 不知道 a 和 b 的"加法"是哪个加法。是自然数的加法？整数的加法？有理数的加法？矩阵的加法？每种加法都是一个不同的类型类实例。

解决：

-- 错误写法
example (a b : Nat) : a + b = b + a := by
  ring  -- 报错！ring 不知道你用的是哪个环

-- 正确写法
example (a b : Nat) : a + b = b + a := by
  omega  -- omega 专门处理 Nat 的线性算术

-- 或者更通用的写法
example (a b : Nat) : a + b = b + a := by
  simp [add_comm, add_left_comm, add_assoc]

核心教训： Lean 的类型类推断是启发式的，不是完备的。当你遇到 failed to synthesize instance 时，不要怀疑 Lean 坏了，是你在某个地方让 Lean 无法推断类型类。

坑 4：simp 的"过度简化"

simp 是 Lean 中最常用的策略（tactic），也是最危险的一个。

症状： 你写 simp，它"证明"了一个错误的目标。或者它把目标简化成了完全无法继续的形式。

根因： simp 使用全局的 simp 集合（simp set），这个集合包含数百条引理。在某些情况下，simp 会应用你意想不到的引理，导致目标被错误的"简化"。

解决：

-- 危险写法：无限制的 simp
simp  -- 可能应用任何 simp 引理

-- 安全写法：带限制的 simp
simp [my_lemma1, my_lemma2]  -- 只使用指定的引理
simp [-undesired_lemma]  -- 禁止使用某个引理

-- 最佳实践：用 simp? 预览
simp?  -- 显示 simp 会使用哪些引理，然后你可以选择

经验法则： 在证明的关键步骤，永远不要用裸 simp。用 simp [explicit_lemmas] 或 simp?。

坑 5：rw 的匹配失败

rw (rewrite) 是另一个高频策略，但它的匹配逻辑让人头疼。

症状： rw [h] 报错 rewrite did not find any occurrence of the pattern，但你可以肉眼看到目标里确实有 h 的左边模式。

根因： rw 是语法匹配，不是语义匹配。a + b 和 b + a 在语法上不同，rw [add_comm] 只会匹配第一个，不会匹配第二个（除非你明确写 rw [add_comm a b]）。

解决：

-- rw 匹配不到时，尝试
rw [← h]  -- 反向匹配
rw [h] at *  -- 在所有假设和目标中匹配
simp [h]  -- 用 simp 代替 rw，simp 更灵活

坑 6-10：速览

篇幅有限，剩余 5 个坑简述如下：

坑 6：calc 块的缩进地狱。 calc 块的缩进规则极其严格，多一个空格就报错。解决：用 VS Code 的 Lean 4 格式化快捷键（Shift+Alt+F），不要手动缩进。

坑 7：match 的覆盖率检查。 Lean 的 match 强制要求所有情况都被覆盖，即使是数学上不可能的情况。解决：用 nomatch 排除不可能的情况，或用 match ... with 的 _ 通配符覆盖。

坑 8：termination_by 的证明义务。 递归函数必须提供终止证明。对于复杂的递归（如 Ackermann 函数），终止证明比函数本身更难写。解决：先用 partial 声明（跳过终止检查），功能验证通过后再回头补充终止证明。

坑 9：ring 和 field 的适用性。 ring 只能用于环（Ring），field 只能用于域（Field）。如果你在自然数（Nat）上用 ring，会报错，因为 Nat 不是环（没有减法）。解决：在 Nat 上用 omega 或 arith，在有理数/实数上用 ring/field。

坑 10：Mathlib 的 API 变更。 Mathlib4 的 API 还在快速演化中，你看到的 6 个月前的教程可能已经过时。解决：用 #check 检查函数的当前签名，关注 Mathlib4 的 GitHub changelog。

推荐学习路径

如果你要学 Lean，这是我推荐的路径：

  1. Natural Number Game (1-2 天): 在浏览器中玩游戏学 Lean 基础语法。不需要安装任何东西。
  2. Mathematics in Lean (1-2 周): 官方教程，覆盖本科数学的各个领域。边读边在 VS Code 中练习。
  3. Mathlib4 文档 + 小项目 (1-2 月): 选一个你熟悉的数学领域（比如线性代数或群论），尝试形式化一些基本定理。遇到不懂的函数就在 Mathlib4 文档中查。
  4. 参与社区 (长期): Lean Zulip 聊天室非常活跃，提问通常能在 1 小时内得到回复。

结尾

Lean 的学习曲线确实陡峭，但越过第一个坡之后，你会发现形式化证明有一种独特的满足感——当你看到 No goals 出现在屏幕上时，你知道你的证明是 100% 正确的，没有漏洞，没有隐藏的假设，没有"显然易见"的跳跃。

这种确定性，在纸笔数学中是不存在的。

推荐资源：Natural Number Game (https://adam.math.hhu.de), Mathematics in Lean (https://leanprover-community.github.io/mathematics_in_lean), Lean Zulip (https://leanprover.zulipchat.com)