Mathlib

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

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

接入

lake new myproject math

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

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

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

找某个定理属于哪个模块：在 Mathlib 文档站搜索它，页面顶部有模块路径。

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

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

基本规则

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

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 的方向

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

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

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

组合示例

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?

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

前一章讲过。最直接，但只找能立即用上的。

2. Loogle：按类型搜

loogle.lean-lang.org —— 按「形状」搜索定理：

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

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

编辑器里也能用：

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

3. Moogle：自然语言搜

moogle.ai —— 用自然语言描述你要的定理，语义搜索 Mathlib。

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

4. 文档站与源码

Mathlib4 文档有全文搜索。

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

提问也是一种检索。 Lean 社区的 Zulip 极其活跃，#new members 频道对初学者友好，通常几小时内有人回答。

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

代数结构层次

Mathlib 用类型类组织代数结构：

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

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

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

-- ✅ 只要求 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 的核心设计原则——定理应该在它成立的最一般的结构上陈述。

常用命名空间

open Nat Int Real Finset BigOperators

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

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

数系记号

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

数系之间的强制转换（coercion）是常见困惑点。

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

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

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。

贡献 Mathlib

流程简述：

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

硬性要求：

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

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

实用片段

-- 查一个定理的完整陈述
#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 搜符号

下一篇：元编程与宏。

本页目录