mathlib 完整入门指南：如何用 Lean 3 数学组件库写出第一个机器可验证的证明

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

你有没有想过这样一个问题：纸上的数学证明，你真的敢说每一步都对吗？哪怕是最细心的人，也可能在某个等式、某个符号上悄悄犯错。而mathlib这个 Lean 3 数学组件库，给了你一个近乎疯狂的承诺——让电脑替你审查证明的每一个环节，错一步都过不了编译。这不是科幻，这是一个真实存在、被全球数学家共同维护了多年的开源项目。本文不绕弯子，直接带你搞清楚它是什么、为什么值得学，以及如何在 30 分钟内跑起来并写下你的第一个形式化证明。

别再问了：mathlib 到底是什么？

简单说，mathlib 是 Lean 3 定理证明器配套的"数学组件库"，它把从自然数加法到群论、拓扑、测度论的一大片数学，全部翻译成了机器可以验证的代码。你写的不再是"我认为这个命题显然成立"，而是"请检查我给出的推导过程"。

一句话理解：mathlib = 一本会自己纠错的数学百科全书。

项目里几十万行 Lean 代码，全部经过严格审查与机器验证，分布在清晰分层的目录中：

它不是给机器看的代码垃圾，而是写给人类读的数学——每个定理都带文档注释和命名规范，读起来像一本结构严谨的教科书。

为什么一个"过时"的库还值得你花时间？

必须诚实告诉你：这个仓库对应的是Lean 3 时代的 mathlib，项目 README 里明确写着"Lean 3 与 mathlib 3 已不再积极维护，新项目请转向 mathlib4"。那为什么还要学它？三个理由足够有分量：

第一，它是理解现代数学库的"源码级教材"。今天的 mathlib4 正是从这个项目演化而来的，无数核心设计——命名规范、模块划分、战术体系——都在这份代码里定型。看懂 mathlib 3，你再看 mathlib4 会轻松非常多。

第二，这里躺着大量"可复现的杰作"。项目 archive/imo/ 里收录了从 1959 年到 2021 年 30 多道国际数学奥林匹克竞赛题的形式化证明；archive/wiedijk_100_theorems/ 里则是"一百个著名数学定理"挑战的成果，比如 perfect_numbers（完全数）、herons_formula（海伦公式）、konigsberg（柯尼斯堡七桥问题）。这些例子体量小、目标明确，是最佳学习素材。

第三，形式化思维本身是稀缺能力。用 mathlib 写证明，你会被迫把"显然"两个字从词典里删掉——这种严谨性，对任何做研究、写代码的人都是一种降维打击。

小结：学它，不是为了用它做新项目，而是为了用最直接的方式理解"机器如何理解数学"。

最快跑起来：三分钟环境搭建

整个上手过程其实就两步：装工具链，拉代码。推荐用leanproject管理依赖，它会自动处理 Lean 版本匹配问题。

第一步，克隆仓库（这是本项目在 gitcode 的镜像地址）：

git clone https://gitcode.com/gh_mirrors/ma/mathlib cd mathlib

第二步，拉取依赖与编译缓存：

leanproject get-deps leanproject build

这里有个能帮你省下大量时间的关键点：mathlib 源码量很大，本地全量编译可能耗很久。leanproject会优先下载官方编译好的 olean 缓存文件，你只需要编译自己改动的部分。如果只想去archive/或某个子目录里探索，可以用项目自带的 scripts/mk_all.sh 脚本批量生成all.lean汇总导入文件，一次编译整个子目录。

编辑器方面，VSCode 装好 Lean 插件即可获得实时错误提示、自动补全和鼠标悬停查看类型的能力——这也是写 Lean 最重要的"驾驶舱"。

小结：装好工具、拉到代码，你就拥有了一个能跑、能查、能改的完整数学库。

第一个证明：让机器替你检查

代码不多，但信息量很大。打开一个.lean文件，输入下面这段（它真实存在于 mathlib 的常用写法中）：

import data.nat.basic open nat -- 交换律：m + n = n + m，机器替你验证 example (m n : ℕ) : m + n = n + m := add_comm m n

add_comm是库里早就证明好的定理，这一行等于告诉 Lean："我要证交换律，它已经在库里了，你检查一下我引用得对不对。" 光标移到上面，VSCode 会给出绿色对勾——证明通过。

想看看真实项目里的完整证明长什么样？打开 archive/imo/imo1959_q1.lean，这是 IMO 1959 第一题："分数 (21n+4)/(14n+3) 对任意自然数 n 不可约"。它的核心思路是证明分子分母互素：

import tactic.ring import data.nat.prime lemma calculation (n k : ℕ) (h1 : k ∣ 21 * n + 4) (h2 : k ∣ 14 * n + 3) : k ∣ 1 := have h3 : k ∣ 2 * (21 * n + 4), from h1.mul_left 2, have h4 : k ∣ 3 * (14 * n + 3), from h2.mul_left 3, have h5 : 3 * (14 * n + 3) = 2 * (21 * n + 4) + 1, by ring, (nat.dvd_add_right h3).mp (h5 ▸ h4)

注意到by ring了吗？这就是 mathlib 的战术（tactic）威力——整式化简交给机器，你只需要给出关键步骤。

小结：写 Lean 证明就像搭积木，你负责思路，战术和已证定理负责苦力。

模块地图：如何在 src/ 里快速找到你要的定理

写证明最常卡住的不是"怎么证"，而是"这个定理叫什么、在哪个文件里"。记住两个规律，立刻少走一半弯路：

• import 路径 = 文件路径。想用src/data/nat/prime.lean里的内容，就写import data.nat.prime。
• 想不起名字就用#check。在文件里敲#check add_comm，Lean 会直接告诉你这个定理的类型签名；配合#find还能按关键词搜索。

再给一张"找东西"速查表：

小结：记住"路径即导入、名字用 #check"，你就能在这座代码迷宫里自由穿行。

新手最容易踩的四个坑（避坑清单）

这部分是用真金白银的编译错误换来的，建议收藏：

1. 最大的坑：版本错位。这个仓库绑定 Lean 3（leanpkg.toml 里写着leanprover-community/lean:3.51.1）。网上大量新教程讲的是 Lean 4 语法，直接照搬必然报错。用elan管理多个 Lean 版本，并确认当前项目激活的是 3.51.1。
2. 导入路径写错。文件名是basic.lean，导入就是import data.nat.basic，不要带.lean后缀、不要把斜杠写成别的分隔符。
3. 头铁全量编译。别一上来就lean --make全库，先leanproject build用缓存，再配合 scripts/mk_all.sh 局部编译。
4. 忽略文档的"已迁移"提示。仓库里 docs/install/ 和 docs/theories/ 的 README 都标注了内容已迁移，本地真正可读的教程在 docs/tutorial/ 和 docs/contribute/，别在空目录里浪费时间。

小结：版本对齐、路径正确、善用缓存、认准有效文档，你就能绕开 80% 的新手事故。

进阶之路：从一行 lemma 到一百个著名定理

跑通第一个证明之后，最有效的进阶路线是这样的：

• 第一周：在 archive/wiedijk_100_theorems/ 里挑一个证明最短的定理（比如 partition 或 ballot_problem），逐行读懂，然后关掉文件自己重写一遍。
• 第二周：去 archive/imo/ 选一道你熟悉的数学题，先自己写思路，再用#check寻找库里现成的引理拼装证明。
• 之后：浏览 docs/contribute/style.md 了解命名与风格规范——读别人的规范，是最快的"内化"方式。

现在，轮到你了

把这篇指南变成行动，你只需要四步：

1. 克隆仓库、装好leanproject，完成环境搭建；
2. 新建一个.lean文件，写下example (m n : ℕ) : m + n = n + m := add_comm m n，亲眼看到绿色的通过标记；
3. 打开 archive/imo/imo1959_q1.lean，把它的证明从头到尾读一遍；
4. 从 docs/tutorial/ 挑一个入门文件，开始你的第一个独立证明。

最后提醒你一个最常见的误区：形式化证明不是"把数学变成编程"，而是"把严谨变成默认配置"。你不是在学一门新语言，而是在重新学习如何不欺骗自己。

还记得开头那个问题吗？现在，电脑能替你的证明背书了。那么——你的第一个机器可验证的证明，打算从哪道题开始？🚀

每一个伟大的数学发现，都始于一个被机器认真对待的小证明。

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