Mathlib4 截至 2024 年末已收录超过 16 万条定理、引理和定义。面对这个规模，手工翻阅文档或凭经验猜名字的效率极低。Lean 4 工具链和 Mathlib 生态提供了一套完整的搜索机制：从编辑器内的 exact?、apply?、rw?、simp?，到浏览器端的 Loogle 和 Moogle——每种工具针对不同的查询意图。掌握这套机制是高效使用 Mathlib 的基本工作方式。

本篇是"深入 Lean"系列第 09 篇。前置阅读：04 核心 tactic 精讲（exact/apply/rw 的语义）、05 simp 与 norm_num（simp 引擎工作原理）、02 Term-mode 与 Tactic-mode 切换心法（两种证明模式的区别）。

问题规模

Mathlib4 的 GitHub 仓库目前约有 70 万行 Lean 代码，模块数量接近 4000。定理覆盖了代数、数论、分析、拓扑、组合、范畴论等数十个领域。一条具体的引理，如 List.length_append 或 Nat.add_comm，隐藏在数百个文件中的某一处。

这个规模带来两个实际问题。第一，即便知道某个事实在 Mathlib 中肯定存在，也不知道它叫什么名字。第二，即便记得名字的大致形状，也可能因为命名空间或参数顺序不同而搜不到。搜索工具解决的正是这两个问题。

编辑器内搜索：`exact?`

exact? 是最直接的工具：给定当前目标，它在 Mathlib 中查找能够一步关闭该目标的项（term）。

import Mathlib

example (n : ℕ) : n + 0 = n := by
  exact?

在 VS Code + Lean4 插件下，光标停留在 exact? 这一行时，InfoView 会显示类似如下内容：

1	`Try this: exact Nat.add_zero n`

点击建议，编辑器会自动将 exact? 替换为 exact Nat.add_zero n。这一步替换非常重要：exact? 是搜索调用，每次编译都会触发一次全库扫描，在大型文件里显著拖慢编译速度；找到目标后应立即用具体引理名替换掉 exact?，只保留搜索结果。

exact? 的底层机制是对当前目标类型做 unification 搜索。它要求找到的项与目标类型完全一致，不允许遗留子目标。如果目标需要先做若干变换才能和已知引理匹配，exact? 通常搜不到，此时需要换 apply?。

InfoView 目标状态解读

exact? 生效前，InfoView 显示：

1	`⊢ n + 0 = n`

exact Nat.add_zero n 关闭目标后，InfoView 显示：

1	`Goals accomplished 🎉`

目标消失即证明完成。如果 exact? 返回的建议执行后目标仍然存在，说明 unification 出了偏差，需要检查建议中的参数是否与当前上下文一致。

编辑器内搜索：`apply?`

apply? 搜索的是结论（conclusion）能与当前目标合一的引理，允许引理有前提（hypothesis）遗留为新子目标。这是与 exact? 的核心区别：exact? 要求完全关闭目标，apply? 只要求引理的结论部分匹配。

1 2	`example (h : 2 ∣ 6) : 2 ∣ 12 := by apply?`

InfoView 可能给出：

1
2
3

Try this: exact dvd_trans h (by norm_num)
-- 或者
Try this: Dvd.dvd.trans h (by norm_num)

也可能出现多条候选。InfoView 会按置信度排列，选择最上方的建议通常是正确的起点。

apply? 比 exact? 慢，因为它的搜索空间更大——几乎所有引理的结论都可能与某个目标匹配。在目标比较通用（如 ⊢ a = b）时，apply? 可能返回几十条候选，需要人工筛选。

实际操作中，先用 exact?，如果没有结果再换 apply?，找到候选后立即替换为具体调用。

`rw?` 与 `simp?`

`rw?`

rw? 搜索可以用于当前目标的重写引理（即等式或 iff 形式的引理）。

1 2	`example (a b : ℕ) : a + b = b + a := by rw?`

InfoView 可能提示：

1	`Try this: rw [Nat.add_comm]`

rw? 只关心当前目标的顶层结构能否被某条等式引理重写，搜索范围比 apply? 窄，因此速度相对快些。找到建议后同样应替换为具体的 rw [...] 调用。

`simp?`

simp? 不是搜索单条引理，而是运行 simp 引擎，然后报告它实际使用了哪些 simp 引理，同时给出等价的 simp only [...] 调用。

1 2	`example (a b c : ℕ) : (a + b) + c = a + (b + c) := by simp?`

InfoView 输出类似：

1	`Try this: simp only [Nat.add_assoc]`

simp? 的价值在于将一次不透明的 simp 调用替换为显式的 simp only [...]，使证明依赖关系可见，也使后续维护更容易——当 Mathlib 版本升级后，simp only [...] 比裸 simp 更不容易因新增 simp 引理而行为改变。

simp? 和 simp 运行相同的引擎，因此速度相近，比 exact?/apply? 快得多。

浏览器端搜索：Loogle

Loogle 是 Mathlib 的在线类型签名搜索引擎，支持在不打开 Lean 编辑器的情况下按类型查找引理。

查询语法

Loogle 的查询语言基于类型表达式，支持以下几种形式：

按名称碎片搜索：直接输入名称片段，如 add_comm，返回所有名称中含此片段的定义。

按类型搜索：输入完整类型表达式，如 ?n + ?m = ?m + ?n，其中 ?n、?m 是通配符变量。Loogle 返回类型与该模式可合一的引理。

按子项搜索：输入 List.length, Nat.succ 等，返回类型中同时含有这两个子项的引理。

示例

查询 ?a * ?b = ?b * ?a，Loogle 返回：

1
2
3

Nat.mul_comm : ∀ (n m : ℕ), n * m = m * n
Int.mul_comm : ∀ (a b : ℤ), a * b = b * a
mul_comm : ∀ {α : Type u_1} [inst : CommMul α] (a b : α), a * b = b * a

最后一条是最通用的版本，适用于任何满足 CommMul 类型类的类型。在 Mathlib 证明中，通常优先用最通用的版本，让类型类机制自动特化。

查询 List.map, List.append，返回类型中同时涉及 List.map 和 List.append 的引理，其中包括：

1 2	`List.map_append : ∀ {α β : Type u_1} (f : α → β) (l₁ l₂ : List α), List.map f (l₁ ++ l₂) = List.map f l₁ ++ List.map f l₂`

Loogle 的搜索结果直接链接到对应的 Mathlib4 文档页面，可以查看完整声明、证明和所在模块。

自然语言搜索：Moogle

Moogle 是针对 Mathlib 的自然语言语义搜索工具。与 Loogle 的类型匹配不同，Moogle 接受自然语言描述，如：

1	`commutativity of addition on natural numbers`

或中文描述（支持程度有限）：

1	`自然数加法交换律`

Moogle 使用向量嵌入模型对查询和引理文档字符串进行语义匹配，返回最相关的候选引理及其文档链接。

Moogle 适合在用户不确定数学术语的精确英文表达时使用，也适合描述"某种性质"而非具体类型签名的场景。其搜索结果的精确度通常低于 Loogle，但覆盖的语义范围更宽。

在实际工作流中，Loogle 和 Moogle 互补：Loogle 用于类型明确的情况，Moogle 用于概念模糊的情况。

用 `#check` 验证引理签名

找到引理名后，在 Lean 文件中用 #check 查看完整签名是验证是否找对的标准步骤。

import Mathlib

#check @List.map_append
-- List.map_append : ∀ {α : Type u_1} {β : Type u_2} (f : α → β)
--   (l₁ l₂ : List α), List.map f (l₁ ++ l₂) = List.map f l₁ ++ List.map f l₂

#check @Nat.add_comm
-- Nat.add_comm : ∀ (n m : ℕ), n + m = m + n

@ 前缀使所有隐式参数显式化，可以看清完整的参数列表和宇宙多态性。不带 @ 的 #check List.map_append 只显示用户可见的类型，隐式参数被折叠。

#print axioms 显示某个定理最终依赖的公理集合，这在需要核查证明不依赖经典逻辑或选择公理时有用：

1 2	`#print axioms Nat.add_comm -- 'Nat.add_comm' depends on axioms: [propext, Quot.sound, Nat.rec]`

Nat.add_comm 仅依赖构造主义公理，没有用到 Classical.choice 或排中律，这与它的直接归纳证明一致。

Mathlib 命名约定

Mathlib 有一套严格的命名约定，理解之后可以直接猜出许多引理的名字，不需要搜索工具。

基本规则

命名格式通常是 Namespace.operation_property 或 Namespace.lhs_description。

Nat.add_comm：自然数加法交换律（add 是运算，comm 是性质）
Nat.add_assoc：自然数加法结合律
Nat.mul_zero：乘法零元（n * 0 = 0）
Nat.zero_mul：零元乘法（0 * n = 0）——注意参数顺序体现在名字里
List.length_append：(l₁ ++ l₂).length = l₁.length + l₂.length
List.map_append：map 与 append 的分配律
List.map_map：map 与 map 的复合规律

参数顺序编码

当两个参数顺序不同时对应不同引理，Mathlib 通过名字区分：mul_zero 对应 a * 0 = 0，zero_mul 对应 0 * a = 0。这使得仅凭目标的结构形状就能猜出引理名。

下划线连接语义成分

复合性质用下划线连接，如 add_left_comm（加法左交换律：a + (b + c) = b + (a + c)）、mul_add（乘法对加法的左分配律）、add_mul（乘法对加法的右分配律）。

常见后缀

_comm：交换律
_assoc：结合律
_left/_right：指定操作位置
_zero/_one：与零或单位元的关系
_succ：与后继的关系
_iff：等价形式（返回 P ↔ Q 而非 P = Q）

掌握这套约定后，很多时候不需要工具，直接在 by exact Nat.add_comm n m 或 rw [List.map_append] 里试一下即可验证猜测是否正确。

term-mode 与 tactic-mode 的对比

搜索工具找到引理名后，既可以在 tactic-mode 下使用，也可以在 term-mode 下直接组合。

以证明 ∀ (a b c : ℕ), a + b + c = a + (b + c) 为例：

tactic-mode：

1 2	`example (a b c : ℕ) : a + b + c = a + (b + c) := by rw [Nat.add_assoc]`

InfoView 在 rw [Nat.add_assoc] 执行后显示：

1	`Goals accomplished 🎉`

term-mode：

1 2	`example (a b c : ℕ) : a + b + c = a + (b + c) := Nat.add_assoc a b c`

两种写法在内核层面等价，生成相同的证明项。term-mode 对于单步引理应用往往更简洁；tactic-mode 在需要多步变换或分情况讨论时结构更清晰。

搜索工具（exact?、apply?、Loogle）返回的建议通常是 tactic-mode 形式，但找到的引理名可以直接移植到 term-mode。

实践工作流

面对一个未知如何证明的目标，以下流程覆盖了绝大多数情形：

目标明确且简单时，先运行 exact?，等待 InfoView 建议，接受后替换为具体调用。如果 exact? 超过约 10 秒没有返回，中断并改用 apply?。

apply? 返回候选后，观察候选引理的结论是否与目标形状匹配，选择最贴近的一条，执行后检查剩余子目标是否可以用 norm_num、simp、或再一次 exact? 关闭。

如果编辑器搜索工具均无结果，切换到 Loogle：将目标类型直接粘贴为查询，或提取其中的关键函数名作为组合查询。Loogle 返回结果后，用 #check @lemma_name 在编辑器中验证签名。

如果连目标涉及的数学概念的英文表达都不确定，用 Moogle 输入自然语言描述，得到候选引理名后再回到 Loogle 或 #check 精确核查。

最后的兜底手段是按命名约定手工猜测：目标是 f (l₁ ++ l₂) 的形状时，试 Xxx.f_append；目标是 a ∘ b 的复合形状时，试 Function.comp_xxx 或 Xxx.map_comp。

整个流程可以简化为：

目标
  → exact? / apply?（编辑器内，30秒上限）
  → Loogle（类型签名）
  → Moogle（自然语言）
  → 命名约定猜测
  → 翻 Mathlib 文档 / 提问社区

每次搜索成功后立即将搜索 tactic 替换为具体引理调用，保持文件编译速度。

完整示例：从目标到证明

以证明 List.map f (l₁ ++ l₂) = List.map f l₁ ++ List.map f l₂ 为例，展示完整的搜索与验证过程。

第一步：写出目标框架

import Mathlib

variable {α β : Type*} (f : α → β) (l₁ l₂ : List α)

example : List.map f (l₁ ++ l₂) = List.map f l₁ ++ List.map f l₂ := by
  exact?

InfoView（exact? 运行中）：

1	`⊢ List.map f (l₁ ++ l₂) = List.map f l₁ ++ List.map f l₂`

InfoView（exact? 返回结果）：

1	`Try this: exact List.map_append f l₁ l₂`

第二步：替换并验证

1 2	`example : List.map f (l₁ ++ l₂) = List.map f l₁ ++ List.map f l₂ := List.map_append f l₁ l₂`

InfoView：

1	`Goals accomplished 🎉`

第三步：用 #check 确认签名

1
2
3

#check @List.map_append
-- List.map_append : ∀ {α : Type u_1} {β : Type u_2} (f : α → β)
--   (l₁ l₂ : List α), List.map f (l₁ ++ l₂) = List.map f l₁ ++ List.map f l₂

签名与目标完全吻合，证明正确。这也顺带示范了 term-mode 写法：List.map_append f l₁ l₂ 直接作为 proof term，无需 by 块。

习题

以下三道习题按难度递增排列，建议先尝试用搜索工具找到引理，再手工验证。

习题 1

证明以下命题，要求找到具体引理名（不使用 simp 或 omega）：

1
2
3

example (n : ℕ) : n * 1 = n := by
  -- 提示：Loogle 查询 ?n * 1 = ?n
  sorry

习题 2

证明以下关于 List.reverse 的引理，要求先用 exact? 或 Loogle 找到相关引理，再组合：

example {α : Type*} (l₁ l₂ : List α) :
    List.reverse (l₁ ++ l₂) = List.reverse l₂ ++ List.reverse l₁ := by
  -- 提示：搜索 List.reverse_append
  sorry

习题 3

以下目标涉及整数除法，尝试用 Loogle 查询 Int.ediv 相关引理，找出 n / 1 = n 的正确引理名，然后补全证明：

1
2
3

example (n : ℤ) : n / 1 = n := by
  -- 提示：Loogle 查询 Int.ediv, 1
  sorry

三道习题的 sorry 均为待填写的占位符，读者替换为搜索到的引理调用后，Lean 会验证证明的正确性。

参考资料

Mathlib4 文档主页：https://leanprover-community.github.io/mathlib4_docs/
Loogle 在线搜索：https://loogle.lean-lang.org/
Moogle 自然语言搜索：https://www.moogle.ai/
Mathlib 命名约定文档：https://leanprover-community.github.io/contribute/naming.html
本系列相关篇：04 核心 tactic 精讲、05 simp 与 norm_num、08 自定义 tactic 与宏
下一篇：10 类型类层次：从 Monoid 到 Field