用 mathlib 把数学证明交给机器检查：3个场景带你入门形式化证明

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

是不是每次写完一道证明题，心里总有点不踏实——"这一步交换顺序真的合法吗？""这个边界情况是不是漏了？"传统纸笔证明的严谨性，全靠作者本人的细心程度兜底，而人恰恰是最容易粗心的。mathlib这个开源数学组件库，把"证明"变成了一门可以逐行验证的语言：你写的每一行推导，计算机都会替你检查，任何逻辑漏洞都藏不住。今天我们就用三个真实场景，看看它是怎么做到的。

传统的数学证明，到底难在哪？

写论文、做习题时，我们最怕的不是"不会证"，而是"证错了自己还不知道"。比如交换求和顺序、处理极限换序、断言某个不等式"显然成立"——这些"显然"往往就是错误的藏身处。更麻烦的是，一份长证明动辄几十步，审稿人或同学未必有耐心逐行核对。

mathlib 的解法很直接：把数学对象（自然数、实数、集合、拓扑空间……）和命题全部编码成机器可读的形式，然后用 Lean 证明助手逐条验证。你的证明不再是给人看的一团文字，而是可以通过编译的程序。机器说"过"，这个结论在逻辑上就站得住。

场景一：让机器替你检查每一步推导

先看一个最简单的例子。过去你证明"任何数加 0 等于它自己"，靠的是直觉；在 mathlib 里，它长这样：

example (n : ℕ) : n + 0 = n := by simp

一行代码，simp战术自动完成化简。别小看这个例子——它的意义在于：证明和运行程序是同一件事。你写的每个lemma、每个example，Lean 都会在后台做类型检查，证明有缺口就报错，绝不蒙混过关。

这种"机器代验"的特性，让数学写作变成了一种自我纠错的过程。就像写代码时编译器帮你抓 bug 一样，写证明时 mathlib 帮你抓逻辑漏洞，而且是立刻、当场、毫不留情。

场景二：像搭积木一样组合现成定理

真正让 mathlib 强大的，是它庞大的"定理仓库"。从基础的数论、代数，到拓扑、测度论，几十万条已证明的定理等着你直接调用，你不需要从公理重新发明轮子。

看一个真实例子。项目里收录了历届 IMO 竞赛题的形式化证明，比如 1960 年第一题，它把题目描述编码成这样：

import data.nat.digits def problem_predicate (n : ℕ) : Prop := (nat.digits 10 n).length = 3 ∧ 11 ∣ n ∧ n / 11 = sum_of_squares (nat.digits 10 n)

这段代码在说："n 是三位数、能被 11 整除、且 n/11 等于各位数字平方和"。接下来，作者不需要手工枚举所有三位数，而是借助库里的linarith（线性不等式求解器）、norm_num（数值计算）等工具，把几百个候选值一次清空。

这种写法的好处是可复用：今天证明竞赛题，明天证明自己的研究结论，过程完全一致。你只需要关心"怎么把命题翻译成代码"，剩下的推理由库和战术替你分担。示例都放在archive/imo/目录下，闲暇时翻一翻，比看十篇论文都涨经验。

场景三：让自动化战术替你算

很多人以为形式化证明要手写每一步，其实大可不必。mathlib 内置了一整套自动化战术，专门处理"繁琐但机械"的推导：

举个例子，证明"x 小于 5 且 x+y 大于 10，则 y 大于 5"：

example {x y : ℚ} (h1 : x + y > 10) (h2 : x < 5) : y > 5 := by linarith

linarith一条命令搞定。你在草稿纸上要做的移项、合并、比较，它几毫秒内完成。这些战术的用法细节，可以查阅docs/tactics.md，也可以直接看test/目录里海量的实战用例。

怎么装才能少踩坑？

上手动线其实很短，三步走：

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

建议配合 VSCode 的 Lean 插件使用，编辑器会实时显示每个sorry（未完成证明）和错误提示，体验接近"带语法高亮的数学草稿纸"。初次构建要编译整个库，等待时间较长属正常现象，耐心等它跑完即可。

新手最容易踩的 3 个坑

1. 版本不对，一切白搭。这个仓库是 Lean 3 时代的版本，官方已停止维护，新项目请优先考虑 Lean 4 与 mathlib4。学旧版本可以读代码、理解思想，但别在上面写新作品。

2.simp不是万能的。它只处理"定义展开 + 库里的简化引理"能覆盖的情况，遇到非平凡代数变换会罢工。这时候换rw手动指路，或者拆成若干have小步，往往比硬碰硬更快。

3. 报错信息看不懂就先#check。碰到"类型不匹配"，别急着改代码，先用#check查一下目标表达式的类型，往往一眼就能发现是ℕ和ℤ混用、还是括号层级错位这类低级问题。

常见问答：关于 mathlib 你还会想问

Q：数学不好能学 mathlib 吗？能。它反而强迫你把每个"显然"拆开看，帮你把模糊的直觉变成精确的推理，数学理解会越来越扎实。

Q：我该从哪个文件开始读？推荐archive/imo/的竞赛题解，代码短、目标明确、注释丰富；进阶再看docs/theories/里的专题介绍和src/各模块源码。

Q：形式化证明只能用于"小定理"吗？恰恰相反，这个库证明了 Abel–Ruffini 定理、中心极限定理级别的结论，archive/wiedijk_100_theorems/里还收录了"百大定理"的证明进度，规模完全不是问题。

下一步，试着证明你自己的第一条定理

从打开编辑器写下第一行example开始，让机器帮你验证一次加法交换律；再试着证明一个你手边习题集里的小结论；最后，挑一道你熟悉的 IMO 题，在archive/imo/里找到对应文件，看看别人怎么拆解、怎么用战术。形式化证明带来的不只是"正确"，更是一种把每个推理环节都看得明明白白的思维方式——这种体验，纸笔给不了你。

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