# Mathlib

> 命名约定的解码规则、四种检索手段、代数结构层次，以及如何贡献。

- 作者：David（道雾轩）
- 专栏：Lean 4 从入门到精通（https://daiw.org/manual/lean4.md）
- 最后更新：2026-08-02
- 原文：https://daiw.org/manual/lean4/mathlib
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）

Mathlib 是目前**最大的形式化数学库**——上百万行，覆盖代数、分析、拓扑、数论、范畴论等。用好它是 Lean 实用化的关键。

## 接入

```bash
lake new myproject math
```

```bash
lake exe cache get        # 必须！下载预编译，否则要编译几小时
```

```lean
import Mathlib            -- 全部导入（慢但省心）
-- 或按需
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic
```

<Callout type="warn">
  **`import Mathlib` 会让编辑器变慢**（要加载整个库的环境）。开发时可以接受，但如果卡顿明显，改成按需 import。

  找某个定理属于哪个模块：在 [Mathlib 文档站](https://leanprover-community.github.io/mathlib4_docs/)搜索它，页面顶部有模块路径。
</Callout>

## 命名约定：会读就等于会搜

Mathlib 的定理名是**按内容机械拼出来的**，学会解码就能猜出名字。

### 基本规则

名字由**结论的结构**从左到右描述：

```text
add_comm         : a + b = b + a           加法交换
mul_assoc        : a * b * c = a * (b * c) 乘法结合
add_zero         : a + 0 = a               加零
zero_add         : 0 + a = a               零加
mul_one          : a * 1 = a
sub_self         : a - a = 0
```

**读法：把符号读成单词，从左到右**。`add_zero` = 「add 一个 zero」→ `a + 0 = a`。注意 `add_zero` 与 `zero_add` 是**不同**的定理（哪边是零）。

### 常用词根

| 词 | 符号/概念 |
| --- | --- |
| `add` `sub` `mul` `div` `neg` `inv` | `+` `-` `*` `/` `-a` `a⁻¹` |
| `zero` `one` | `0` `1` |
| `lt` `le` `gt` `ge` | `<` `≤` `>` `≥` |
| `eq` `ne` | `=` `≠` |
| `pos` `neg` `nonneg` `nonpos` | `0 <` `< 0` `0 ≤` `≤ 0` |
| `comm` `assoc` `left` `right` | 交换/结合/左/右 |
| `self` | 两个参数相同 |
| `iff` | `↔` |
| `of` | **从……推出**（方向标记） |
| `cancel` | 消去 |
| `succ` `pred` | 后继/前驱 |

### of 的方向

```text
lt_of_le_of_ne   : a ≤ b → a ≠ b → a < b
--  ^^^^^^^^^^^^  结论在前，of 之后是前提
```

**`X_of_Y_of_Z` 读作「由 Y 和 Z 得到 X」**。这是 Mathlib 最常见的命名模式。

```text
le_of_lt         : a < b → a ≤ b
ne_of_gt         : a > b → a ≠ b
Nat.pos_of_ne_zero : n ≠ 0 → 0 < n
```

### 组合示例

```text
add_le_add       : a ≤ b → c ≤ d → a + c ≤ b + d
mul_pos          : 0 < a → 0 < b → 0 < a * b
add_lt_add_left  : b < c → a + b < a + c
sub_nonneg       : 0 ≤ a - b ↔ b ≤ a
```

猜名字的流程：**写出你要的命题 → 按上表把它读成单词 → 试试那个名字**。命中率相当高。

## 四种检索手段

### 1. exact? / apply? / rw?

```lean
example (a b : ℕ) (h : a < b) : a ≤ b := by exact?
-- Try this: exact Nat.le_of_lt h
```

[前一章](https://daiw.org/manual/lean4/automation)讲过。**最直接**，但只找能立即用上的。

### 2. Loogle：按类型搜

[loogle.lean-lang.org](https://loogle.lean-lang.org/) —— **按「形状」搜索定理**：

```text
|- _ + _ = _ + _          找结论形如 a + b = c + d 的
Nat, List Nat -> _        找接受这两个参数的
"comm"                    按名字子串
Nat.succ, (· + ·)         同时提到这两个的
```

**Loogle 是找不到定理时的第一站**。它比按名字猜更可靠——你只需知道命题「长什么样」。

编辑器里也能用：

```lean
open Lean in
example : True := by
  trivial
-- #loogle 命令（装了对应扩展时可用）
```

### 3. Moogle：自然语言搜

[moogle.ai](https://www.moogle.ai/) —— 用自然语言描述你要的定理，语义搜索 Mathlib。

适合「我知道数学上叫什么，但不知道 Mathlib 里怎么命名」的情况。

### 4. 文档站与源码

[Mathlib4 文档](https://leanprover-community.github.io/mathlib4_docs/) 有全文搜索。

**直接读源码往往最快**——找到相关文件后，附近的定理通常就是你要的。Mathlib 的组织是主题化的。

<Callout type="info">
  **提问也是一种检索。** Lean 社区的 [Zulip](https://leanprover.zulipchat.com/) 极其活跃，`#new members` 频道对初学者友好，通常几小时内有人回答。

  提问时贴上**可复现的最小代码**（含 import），回答质量会高很多。
</Callout>

## 代数结构层次

Mathlib 用[类型类](https://daiw.org/manual/lean4/typeclasses)组织代数结构：

```text
Mul, Add, Zero, One         最基本的运算
  ↓
Semigroup      (结合)
  ↓
Monoid         (+ 单位元)
  ↓
Group          (+ 逆元)
  ↓
CommGroup      (+ 交换)

Semiring → Ring → CommRing → Field
  ↓
Order 层次：Preorder → PartialOrder → LinearOrder
  ↓
拓扑：TopologicalSpace → MetricSpace → NormedSpace
```

**写通用定理时用最弱的假设**：

```lean
-- ✅ 只要求 Monoid，适用范围最广
theorem my_thm [Monoid M] (a : M) : a * 1 = a := mul_one a

-- ❌ 要求 Field，但实际只用到乘法单位元
theorem my_thm' [Field F] (a : F) : a * 1 = a := mul_one a
```

这是 Mathlib 的核心设计原则——**定理应该在它成立的最一般的结构上陈述**。

## 常用命名空间

```lean
open Nat Int Real Finset BigOperators
```

| 命名空间 | 内容 |
| --- | --- |
| `Nat` `Int` `Rat` `Real` `Complex` | 数系 |
| `Finset` `Set` | 有限集/集合 |
| `List` `Array` `Multiset` | 数据结构 |
| `Function` | 函数性质（单射满射等） |
| `BigOperators` | `∑` `∏` 记号 |

```lean
open BigOperators in
example (n : ℕ) : ∑ i in Finset.range n, (1 : ℕ) = n := by simp
```

## 数系记号

```lean
#check (1 : ℕ)     -- Nat      \N
#check (1 : ℤ)     -- Int      \Z
#check (1 : ℚ)     -- Rat      \Q
#check (1 : ℝ)     -- Real     \R
#check (1 : ℂ)     -- Complex  \C
```

<Callout type="warn">
  **数系之间的强制转换（coercion）是常见困惑点。**

  ```lean
  example (n : ℕ) : (n : ℤ) ≥ 0 := by positivity
  ```

  `(n : ℤ)` 里的 `↑` 是自动插入的转换。混合类型的表达式常常需要 `push_cast` / `norm_cast` 来整理：

  ```lean
  example (a b : ℕ) : ((a + b : ℕ) : ℤ) = (a : ℤ) + (b : ℤ) := by push_cast; ring
  ```

  | tactic | 作用 |
  | --- | --- |
  | `norm_cast` | 规范化类型转换，尽量消去 |
  | `push_cast` | 把转换往叶子推 |
  | `exact_mod_cast h` | 忽略转换差异地使用 h |

  **看到目标里有一堆 `↑` 且卡住，先试 `push_cast` 或 `norm_cast`。**
</Callout>

## 贡献 Mathlib

流程简述：

```text
1. 在 Zulip 上说你要做什么（避免重复劳动）
2. fork mathlib4，建分支
3. 写代码，遵守命名与风格约定
4. 本地跑 lake build 与 lint
5. 提 PR，等 reviewer
```

硬性要求：

- **风格**：100 字符行宽、特定的缩进与空格约定，`lake exe lint` 检查。
- **文档字符串**：公开定义必须有 `/-- ... -/`。
- **命名**：严格遵守上面的约定。
- **最弱假设**：定理应在最一般的结构上陈述。
- **不能有 `sorry`**。

Mathlib 的 review 以严格著称——但这正是它质量的来源。首次贡献建议从小的补充引理开始。

## 实用片段

```lean
-- 查一个定理的完整陈述
#check @Nat.add_comm

-- 看定义
#print Nat.gcd

-- 查依赖的公理（确认没 sorry）
#print axioms my_theorem

-- 看某个命名空间下有什么
open Nat in
#check @Nat.succ_le_succ

-- 搜索名字含某子串的定理（Mathlib 提供）
example : True := by
  trivial
-- 在编辑器里用 Ctrl+T / Cmd+T 搜符号
```

下一篇：[元编程与宏](https://daiw.org/manual/lean4/metaprogramming)。