mathlib 实战完全指南：用 Lean 语言把数学证明变成可验证的代码，3 个案例带你入门

mathlib 实战完全指南：用 Lean 语言把数学证明变成可验证的代码，3 个案例带你入门

【免费下载链接】mathlibLean 3's obsolete mathematical components library: please use mathlib4项目地址: https://gitcode.com/gh_mirrors/ma/mathlib

如果你正在寻找一份能真正上手的mathlib教程，那么恭喜你，来对地方了。mathlib 是 Lean 语言最著名的数学组件库，它把群论、拓扑、测度论等庞大的数学体系，全部变成了一行行可被机器自动验证的代码。本文不打算按部就班地罗列安装步骤，而是从一个更扎心的问题讲起：为什么你的手写证明，可能连你自己都信不过？

一、痛点开场：一份写了三页、却没人敢签字的证明

数学系的学生大概都有过这样的经历：花了一个通宵写出一道不等式证明，草稿纸用了七张，每一步都"显然成立"。可当导师追问"第三步为什么成立"时，你只能硬着头皮解释。更麻烦的是，人类证明天然存在盲区——跳步、笔误、想当然的"显然"，这些在考试里或许能蒙混过关，在科研论文里却可能埋下致命的错误。

这正是形式化证明要解决的问题。所谓形式化证明，就是把每一步推理都写成严格、无歧义的代码，交给一个"永不疲倦、绝不徇私"的机器裁判去逐行检查。而 Lean 和它的数学库 mathlib，就是目前最成熟、最活跃的这套"证明裁判系统"之一。用 Lean 证明数学定理，本质上是在和一台苛刻的机器对话：你说"由 AM-GM 不等式可得"，机器会反问"哪个 AM-GM？前提条件满足吗？"

二、先弄明白：mathlib 到底是个什么东西

2.1 它不是"工具箱"，而是一座城市

如果把 Lean 比作一门编程语言，那 mathlib 就是围绕它建起的一座数学城市。城市里有街道（命名空间）、有地标（核心定理）、有市政厅（tactic 战术库）。它的源码规模超过百万行，覆盖了从幼儿园算术到研究生课程的几乎所有数学分支：

这套模块体系可不是随便分的。src/algebra/order/下有几十个文件专门处理序结构与代数结构的交互，src/linear_algebra/matrix/下有三十多个文件专门啃矩阵理论。你想证明的定理，大概率已经有人把前置引理铺好了路。

2.2 机器裁判的三个特点

• 绝不跳步：每一步都必须有依据，要么来自定义，要么来自已证定理，要么来自战术的自动化推理。
• 绝不双标：同一套标准对所有人都一样，你写错一个符号，编译就报错。
• 可复现：证明以.lean文件形式存在，任何人 clone 下来都能重新验证，不需要"相信作者"。

三、纸笔证明 vs 代码证明：一张对比表看清差异

看到这里你可能会问：既然这么麻烦，为什么还有人乐此不疲？答案藏在两个地方：一是数学本身需要这种"可验证的严谨"，二是当你真的跑通一个漂亮证明时，那种"机器认可了我"的爽快感，是纸笔完全给不了的。

四、动手前的准备：mathlib 环境搭建方法（3 步走）

别被"环境搭建"四个字吓到。mathlib 环境搭建方法已经非常成熟，核心就三步。

4.1 装好 Lean 版本管理器

Lean 社区推荐使用 elan 来管理 Lean 版本，它就像 Rust 的 rustup 一样，可以随时切换编译器版本。mathlib 3 锁定在 Lean 3.51.1（见仓库根目录的leanpkg.toml）。

4.2 拉取项目源码

git clone https://gitcode.com/gh_mirrors/ma/mathlib cd mathlib leanproject get-deps

小提示：如果是初学者，建议先用leanproject new my_project创建一个依赖 mathlib 的空项目，而不是直接编译整个库——全库编译一次可能要几十分钟，新手往往等得心慌。

4.3 验证环境

新建一个test.lean，写上一行：

example : 2 + 2 = 4 := by norm_num

如果编辑器（VSCode + Lean 插件）显示绿色的对勾，说明环境通了。这行代码的意思很直白："请证明 2+2=4，用 norm_num 战术自动搞定。"你的形式化证明之旅，就从这条绿色对勾开始。

五、贯穿全文的实战故事：从 1+1 到 IMO 真题

理论说再多都是空谈，我们用一场"三级火箭"式的实战，把 mathlib 的核心玩法串起来。我们的目标是最终证明一道国际数学奥林匹克（IMO）真题——这条路上你会看到 mathlib 真正的威力。

5.1 第一级：热身——让机器听懂"显然"

先证明一个初中生都"知道"的事实：加法结合律。在 Lean 里它长这样：

lemma add_assoc_nat (a b c : ℕ) : (a + b) + c = a + (b + c) := begin induction c with c ih, { simp }, { simp [ih] } end

注意看，我们没有"背"这个结论，而是用归纳法一步步构造证明：先验证c = 0时成立，再假设c时成立、证明c + 1时也成立。simp战术负责处理琐碎的化简。这就是形式化证明的日常：把"显然"拆成机器能接受的"显然"。

5.2 第二级：进阶——让战术替你干活

数学里最爽的时刻，莫过于把繁琐计算甩给自动化战术。看这个例子：

import analysis.special_functions.pow example (x : ℝ) (h : 0 ≤ x) : x ^ 2 ≥ 0 := begin nlinarith end

nlinarith会自动处理非线性算术推理。在src/tactic/目录下，mathlib 维护着上百个这样的战术：linarith解线性不等式、ring做多项式环上的恒等变换、norm_num做数值计算、fin_cases枚举有限情况……学会选战术，比学会写证明更省力。打开 docs/tactics.md 可以查看完整清单。

5.3 第三级：实战——挑战 IMO 2020 第二题

热身完毕，我们直奔主题。mathlib 仓库里有一个专门存放竞赛题证明的目录archive/imo/，里面躺着从 1959 年到 2021 年的几十道真题。其中 IMO 2020 第 2 题是这样的：

实数 a、b、c、d 满足 a ≥ b ≥ c ≥ d > 0 且 a + b + c + d = 1。证明： (a + 2b + 3c + 4d) · aᵃ · bᵇ · cᶜ · dᵈ < 1

纸笔做法的核心是用加权 AM-GM 不等式处理指数项，再用代数恒等式收尾。而在archive/imo/imo2020_q2.lean里，这段证明被压缩成了几十行：

theorem imo2020_q2 (a b c d : ℝ) (hd0 : 0 < d) (hdc : d ≤ c) (hcb : c ≤ b) (hba : b ≤ a) (h1 : a + b + c + d = 1) : (a + 2 * b + 3 * c + 4 * d) * a ^ a * b ^ b * c ^ c * d ^ d < 1 := begin have hp : a ^ a * b ^ b * c ^ c * d ^ d ≤ a * a + b * b + c * c + d * d, by refine geom_mean_le_arith_mean4_weighted _ _ _ _ _ _ _ _ h1; linarith, -- ……中间是加权 AM-GM 的展开与放缩…… ... = (a + b + c + d) ^ 3 : by ring ... = 1 : by simp [h1] end

读这段代码你会发现几件有趣的事：

1. 前提全部显式化：题目里"a ≥ b ≥ c ≥ d > 0"被拆成了hd0、hdc、hcb、hba四个假设，一个都不能少。
2. 定理库直接可用：geom_mean_le_arith_mean4_weighted就是 mathlib 在src/analysis/里早就证明好的加权 AM-GM 引理——前人种树，后人乘凉。
3. by ring与by simp收尾：最后的多项式展开和代入化简，机器眨眼间完成。

这就是为什么这个仓库如此珍贵：一道 IMO 真题的完整、可验证、可复现的证明，就这样安静地躺在archive/imo/里，随时可以被任何学习者打开研究。类似的宝藏还有archive/wiedijk_100_theorems/——著名的"数学百大定理"清单里，欧几里得-欧拉定理（偶数完美数的完全刻画）、生日悖论、三次方程通解等都已在此形式化，对应文件perfect_numbers.lean正是第 70 号定理的证明。

六、效率提升清单：让形式化证明少走弯路的 6 个技巧

跑过上面三个案例，你已经算半个形式化玩家了。下面这份清单能让你的效率再上一个台阶：

• 先搜库，再动笔：证明之前，先在src/里搜索你的目标引理。用#check命令随时查定理签名，用#find按关键词检索。
• 善用have拆解：把大证明切成小引理，每个have都是一个小目标，逐个击破，linarith、ring这类战术在每个小目标上都更高效。
• 用library_search碰运气：当你卡住时，敲library_search，它会在整个 mathlib 里搜索能否直接用某条现成定理解决当前目标——经常有惊喜。
• 归纳法优先：面对自然数命题，induction往往比暴力展开更快，如前面结合律的例子。
• 学会读错误信息：Lean 的报错不是噪音，它是机器在告诉你"还缺什么条件"。把报错里的failed to synthesize看成拼图线索。
• 多逛archive/和docs/tutorial/：docs/tutorial/里有针对初学者的完整 Lean 教程文件（例如Zmod37.lean带你一步步证明模 37 的二次剩余问题），比啃源码轻松得多。

七、学习路线图：从入门到贡献者的三条路径

mathlib 的学习资源就藏在仓库内部，按顺序走，三个月内你就能从零基础到读懂竞赛题证明：

1. 第 1 周：熟悉环境与语法—— 完成 docs/install/ 下的安装文档，跑通 docs/tutorial/ 里的入门示例。
2. 第 1~2 个月：跟着真实证明学—— 打开archive/imo/imo2020_q2.lean，逐行理解；对照src/里的源码，学习社区公认的命名规范和证明风格（可参考 docs/contribute/naming.md）。
3. 第 2~3 个月：尝试小贡献—— 从scripts/port_status.py和docs/100.yaml查看哪些定理还没被形式化，选一个简单的练手。mathlib 社区对新人极其友好，从"补一个simp引理"开始，你会慢慢体会到贡献的快乐。

八、常见问题速查（FAQ）

Q：编译 mathlib 全库太慢怎么办？A：用leanproject new建独立项目，只拉取需要的内容；日常写证明时开启olean缓存（leanproject get-mathlib-cache），能把编译时间从小时级压到秒级。

Q：代码报错了，但我看不出哪里错？A：把错误定位到具体行，检查三件事：括号是否配对、类型是否匹配（ℕ和ℝ不能混用）、是否漏了某个前提假设。80% 的新手报错都出在这三处。

Q：simp和ring有什么区别？A：simp擅长利用库里的等式规则化简表达式；ring专门处理交换环上的多项式恒等变换。记不住就都试一下，反正机器的错误提示会告诉你答案。

Q：这个仓库还能继续贡献代码吗？A：注意！这个仓库是 Lean 3 时代的 mathlib，官方已停止接收新贡献，新开发全部转向 mathlib4（Lean 4 版本）。但它依然是学习形式化证明的绝佳教材——结构清晰、注释详尽、难度梯度合理。

九、写在最后：你的第一个形式化证明，就从现在开始

回顾整篇文章，你会发现一个规律：每一个伟大的数学证明，都始于一行最简单的example。我们从一个2 + 2 = 4的验证，一路走到了 IMO 真题的完整证明——这条路上没有天才，只有"把大目标拆成小目标，让机器帮你逐个击破"的方法论。

现在，轮到你了：

1. 打开终端，clone 一份 mathlib 源码；
2. 新建你的第一个.lean文件，写下example : 1 + 1 = 2 := by norm_num；
3. 盯着那条绿色的对勾，感受一下"机器认可了你"的滋味；
4. 然后，去archive/imo/找一道你最感兴趣的题，试着读懂它，甚至改写它。

形式化证明不会取代数学家的直觉，但它会给你的直觉装上"可验证"的保险丝。当你在深夜敲下最后一行end，看到编辑器里一片绿色时，你会明白——这台机器裁判，正在用最苛刻的方式，见证你对数学最深的诚实。开始吧，你的名字值得出现在下一个 commit 里。🚀

【免费下载链接】mathlibLean 3's obsolete mathematical components library: please use mathlib4项目地址: https://gitcode.com/gh_mirrors/ma/mathlib