向 Mathlib 贡献一条引理，从选题到合并大约需要经历六个阶段：确认缺口、搜索已有引理、写证明、通过本地 lint、跑通 CI、完成 PR 审核。本文以一个具体的 List 辅助引理为例，完整走一遍这条路径。

选题：找一个真实的缺口

Mathlib 的条目超过十五万条，盲目选题很容易踩在别人已经证过的结论上。有效的选题通常来自两个方向：一是在自己的项目里遇到 exact? 无法命中的目标；二是在 Zulip 的 #mathlib4 频道里找标了 easy 标签的 issue。

本文选用的定理是 List.length_zipWith，即：

1
2
∀ (f : α → β → γ) (l₁ : List α) (l₂ : List β),
  (List.zipWith f l₁ l₂).length = min l₁.length l₂.length

在实际的 Mathlib 里，这条结论已经存在（List.length_zipWith），但选它作例子的原因是它足够小、结构清晰，可以完整演示所有步骤，而不会把证明本身的复杂度淹没流程细节。实际投稿时，需要找 Mathlib 确实没有的定理。

搜索已有引理：避免重复劳动

提交一条 Mathlib 已有的引理是 PR 被关闭最常见的原因。正式动笔前需要过以下三关。

用 exact? 和 apply? 探查

在本地的 .lean 文件里写下目标类型，然后用 exact?：

1
2
3
example (f : α → β → γ) (l₁ : List α) (l₂ : List β) :
    (List.zipWith f l₁ l₂).length = min l₁.length l₂.length := by
  exact?

InfoView 面板会列出所有类型能匹配的候选引理。apply? 的作用类似，但它允许目标尚未完全具化，适合在证明中途探路。两个 tactic 都依赖 Lean Language Server 实时索引 Mathlib，第一次运行可能需要等待几秒。

用 Loogle 做全文搜索

Loogle 是 Mathlib 的在线引理搜索引擎，支持三种查询模式：

  • 按名称子串搜索：输入 zipWith length，返回所有名字同时含这两个词的引理。
  • 按类型签名搜索：输入 List.zipWith _ _ _ |>.length，返回结论或前提含该模式的引理。
  • 按参数类型搜索：输入 List α → List β → ℕ，返回所有接受两个 List 并返回自然数的引理。

三种模式可以组合。对 zipWith 系列查一遍之后，如果 Loogle 返回空或返回的条目类型与目标不匹配，说明这条引理确实缺失，可以继续。

在 Mathlib4Docs 上确认

Loogle 依赖索引可能有延迟。最终确认要到 Mathlib4Docs 用全文搜索直接查引理名。命名规范见下一节，知道命名规律后能大幅提高搜索精度。

命名约定与风格指南

Mathlib 的命名规则比多数库更严格，审核者会直接拒绝不符合规范的命名。

命名层级结构

引理名由命名空间 + 谓词 + 参数特征拼成，各部分之间用下划线分隔。例如：

1
2
3
List.length_zipWith      -- 命名空间 List，结论关于 length，涉及 zipWith
Nat.add_comm             -- 命名空间 Nat，结论关于 add，性质为 comm(utativity)
Finset.sum_empty         -- 命名空间 Finset，结论关于 sum，参数为 empty

常见谓词缩写：comm（交换律）、assoc（结合律）、left/right（左/右版本）、zero/one/succ（特化到零/一/后继）、nil/cons（List 特化）。

@[simp] 标注的判断标准

Mathlib 对 @[simp] 有明确的准入条件，不是所有等式引理都适合标注：

  1. 结论必须是等式或 iff，且右侧比左侧"更简单"（结构更小或范式更统一）。
  2. 不引入新的、作用域比左侧更大的变量。
  3. 不与已有 simp 集合产生循环（a = b 和 b = a 同时是 @[simp] 就会死循环）。

List.length_zipWith 是一个典型的好 @[simp] 候选：左侧含复合表达式 (zipWith ...).length，右侧是 min，右侧更接近范式，且不引入新变量。

@[ext]、@[norm_cast] 的作用域

@[ext] 加在"外延相等"引理上，指导 ext tactic 自动展开。@[norm_cast] 加在 coercion 相关等式上，指导 norm_cast 和 push_cast 规范化强制转换。两者都有专门的 lint 检查，误加会触发 warning。

完整的证明文件

实际要提交的 .lean 文件结构如下：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
/-
  File: Mathlib/Data/List/ZipWith.lean  (新增内容)
  Author: <your name>
  License: Apache 2.0
-/

import Mathlib.Data.List.Basic
import Mathlib.Data.Nat.Defs

namespace List

variable {α β γ : Type*}

/-- The length of `List.zipWith f l₁ l₂` equals the minimum of the two input lengths. -/
@[simp]
theorem length_zipWith (f : α → β → γ) :
    ∀ (l₁ : List α) (l₂ : List β),
      (zipWith f l₁ l₂).length = min l₁.length l₂.length
  | [], _        => by simp [zipWith]
  | _ :: _, []   => by simp [zipWith]
  | _ :: t₁, _ :: t₂ => by
      simp only [zipWith, length_cons]
      rw [length_zipWith f t₁ t₂]
      simp [Nat.succ_min_succ]

end List

theorem 和 def 都可以用结构递归写法（多个方程子句），这是 term mode 的做法；也可以在 tactic mode 里用 induction 展开。上面用了 term/tactic 混合写法：外层方程子句是 term mode 的模式匹配，每个分支的 by 引入 tactic 块。

纯 tactic 版本同样合法：

1
2
3
4
5
6
7
8
9
10
11
12
@[simp]
theorem length_zipWith' (f : α → β → γ) (l₁ : List α) (l₂ : List β) :
    (zipWith f l₁ l₂).length = min l₁.length l₂.length := by
  induction l₁ generalizing l₂ with
  | nil => simp [zipWith]
  | cons h t ih =>
    cases l₂ with
    | nil => simp [zipWith]
    | cons h₂ t₂ =>
      simp only [zipWith, length_cons]
      rw [ih t₂]
      simp [Nat.succ_min_succ]

两种写法对 Mathlib 都可以接受，审核者更常见的偏好是：如果模式匹配对应结构明显，用 term mode 的方程子句；如果证明步骤需要大量 rewriting，用 tactic mode。

InfoView 辅助定位

在 VS Code 里把光标放在 simp only [zipWith, length_cons] 行后，InfoView 面板显示的是该行执行后的剩余目标：

1
2
3
4
5
6
7
case cons.cons
α β γ : Type u_1
f : α → β → γ
h : α, t₁ : List α
h₂ : β, t₂ : List β
ih : ∀ (l₂ : List β), (zipWith f t₁ l₂).length = min t₁.length l₂.length
⊢ Nat.succ (zipWith f t₁ t₂).length = min (Nat.succ t₁.length) (Nat.succ t₂.length)

从这个目标可以直接读出 rw [ih t₂] 能将左侧的 (zipWith f t₁ t₂).length 替换为 min t₁.length t₂.length，再用 simp [Nat.succ_min_succ] 收束。InfoView 是调试 tactic 序列最高效的工具，比反复运行整个文件快得多。

本地 Lint

在提交 PR 之前，本地跑 #lint 是必须的。Mathlib 的 lint 工具链远比标准 Lean lint 更细。

基础 #lint 命令

在文件末尾加入：

1
#lint

Lean 会对当前文件跑完整的 Mathlib linter 套件，包括：

  • dupNamespace：检查引理名和命名空间是否重复（如 List.List.foo）。
  • simpNF：检查 @[simp] 引理的左侧是否已经是 simp 范式（如果左侧已能被已有 simp 规则化简，说明这条引理永远不会被触发）。
  • unusedArguments：检查前提里是否有从不使用的变量。
  • docBlame：检查 theorem/def 是否都有文档注释 /-- ... -/。

simpNF 是最容易触发的。例如，如果写了 @[simp] theorem foo : f (g x) = h x，但 f ∘ g 已有一条 simp 规则会把 f (g x) 化简成其他形式，那 simpNF 就会报错，因为 foo 的 lhs 永远不会以"待化简"的形式出现在目标里。

类型类相关 lint

@[ext] 引理需要满足：引理的形式必须是 ∀ x y, (∀ ..., x.field = y.field) → x = y，否则 ext tactic 无法识别。lint 工具会检查 ext 引理的格式。

风格检查

除了 #lint，Mathlib 还要求：

  • 文档注释用 /-- ... -/，不用 -- 。
  • 行宽不超过 100 字符。
  • 前导空格只用空格，不用 Tab。
  • import 按字母序排列（实际上 CI 会自动检查并修正）。

在本地可以用 lake exe lint-style 命令检查风格问题，它会输出具体行号和建议。

CI 流水线

Mathlib 的 CI 跑在 GitHub Actions 上，每次 push 触发。了解 CI 的构成能大幅降低等待时间。

CI 的主要阶段

  1. 构建 Mathlib：Lean 会从 cache 中拉取已有的 .olean 文件（Lean 的编译产物），只重新编译改动文件及其依赖。Mathlib 有专属的 cache server（leanprover-community/mathlib4 的 CI cache），通常不需要从头编译整个库。

  2. lint 检查：对改动文件跑完整 #lint 套件，任何一条 linter 报错都会阻断合并。

  3. 文档生成：检查文档注释能正常渲染为 Mathlib4Docs 格式。

  4. lake build：确认整个 Mathlib 在加入新文件后还能完整构建。

常见 CI 失败原因

simpNF lint 报错是最高频的。修复方式通常是：要么去掉 @[simp]，要么调整引理的方向（把左右侧对调），要么把前提中某个会被 simp 折叠的表达式换成更底层的形式。

timeout 是第二常见的问题，通常出现在 decide 或 omega 被用在大数计算上。这种情况下需要换成手动证明或更高效的 tactic。

sorry 造成的构建失败会被 CI 里的专用检查拦截，Mathlib 会拒绝任何含 sorry 的 PR，包括通过宏间接引入的 sorry（如旧版的 native_decide 在某些情况下会静默展开成 sorry）。

在本地模拟 CI

在本地跑：

1
2
3
lake exe cache get     # 拉取 .olean cache
lake build Mathlib     # 构建整个库（有 cache 时很快）
lake exe lint-style    # 检查代码风格

等到本地 lake build 无报错、#lint 无 error 之后再推送，能大幅减少不必要的 CI 轮次。

PR 流程与审核

开 PR 的前置准备

Mathlib 要求：

  • Fork leanprover-community/mathlib4，在 fork 上建新分支（命名格式通常是 feat/list-zipwith-length）。
  • PR 标题格式：feat(Data.List.ZipWith): add length_zipWith，命名空间放在括号里。
  • 每条 PR 最好只改一个文件或一组强相关文件，改动范围越小，审核越快。

PR 的 description 写法

Mathlib 有 PR 模板，需要填写：

  • 改动内容简述（一句话）。
  • 为什么这条引理有用（应用场景或引用某个 issue）。
  • 如果改动了已有文件，说明是否破坏了向下兼容。

审核流程

Mathlib 用 bors-ng（一个 merge bot）管理合并队列。审核者会在 PR 上留评论，常见的反馈模式：

  • 要求改命名：最常见，审核者会直接给出他们认为正确的名字。
  • 要求加 @[simp] 或去掉 @[simp]：审核者会解释理由，通常是基于 simp 集合的整体一致性。
  • 要求补充文档注释或例子：如果引理的适用场景不显然，会要求加 /-- ... -/ 注释和 example 演示。
  • 要求把证明改得更短：Mathlib 倾向于用 simp 一步完成的证明，而不是多步手动 rewriting。

审核通过后，审核者会用 bors r+ 触发 merge bot，bot 会把 PR 加入合并队列，在 CI 全部通过后自动合并到 main。整个过程通常需要几小时到一两天。

修改与回应

审核意见出现后，直接在同一分支上追加 commit，不需要重开 PR。Mathlib 不要求在提交前 rebase，但合并前 bot 会自动处理 merge conflict。如果审核者要求的改动较大（比如完全重构证明结构），可以先在本地做好再推送，避免碎片化的 commit 堆积。

交叉参考

以下文章与本文内容有较强关联，建议配合阅读：

练习

练习 1：证明 List.length_zip

标准库里 List.zip 是 zipWith 的特化（zip = zipWith Prod.mk）。请不借助 length_zipWith 定理，直接对 List.zip 做结构归纳，证明：

1
2
theorem length_zip_exercise (l₁ : List α) (l₂ : List β) :
    (l₁.zip l₂).length = min l₁.length l₂.length

证明完成后，用 exact? 确认 Mathlib 里是否已有这条引理，并对比名字是否一致。

练习 2：搜索 Nat.add_left_cancel 的等价引理

用三种方式各搜一遍：exact?（在 tactic 块内）、Loogle（Nat add cancel）、Mathlib4Docs（全文搜索 add_left_cancel）。记录三种方式各找到哪些候选，以及它们的类型签名是否完全相同。

练习 3：为一条自定义引理跑 #lint 并修复报错

写下面这条引理（故意不加文档注释，且名字不符合规范）：

1
2
3
theorem myList_len_zip (f : α → β → γ) (a : List α) (b : List β) :
    (a.zipWith f b).length = Nat.min a.length b.length := by
  simp [List.length_zipWith]

在文件末尾加 #lint，观察 docBlame（缺少文档注释）和 simpNF（Nat.min 与 min 在当前环境下是否为 simp 范式）两个 linter 的输出，然后按提示修复，直到 #lint 零报错。

参考资料