企业官网建设流程全解析

mathlib 数学库快速入门指南：把数学证明变成能编译的代码

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

你有没有遇到过这种状况：一道证明题，草稿纸上算了三遍，每次都觉得"这次肯定没问题"，可交上去还是被指出某一步跳得太快？传统上，数学证明靠人眼逐行检查，而人眼恰恰最容易漏掉"显然成立"那一步。那反过来想——如果证明也能像程序代码一样，由机器逐行验证合法性，是不是就再也不用担心自己写错了？这正是 mathlib 数学库在解决的事：它把"写证明"这件事，变成了"写能被编译检查的代码"。

一句话说清：mathlib 到底是个什么库

简单讲，mathlib 是一本用 Lean 语言写成的、每个定理都被机器验证过的"数学百科全书"。它不是一个教学玩具，而是支撑了国际数学奥林匹克题目、百大经典定理等大量形式化证明的组件库。你需要做的，不是背数学知识，而是学会"把数学推理翻译成 Lean 能听懂的话"。

需要先说明一点：当前仓库是Lean 3 时代的 mathlib，官方已停止维护并转向 mathlib4。但这不影响它的学习价值——它的目录结构、命名规范、证明组织方式，至今仍是理解"形式化证明怎么写"最好的标本。

最快路径：十分钟把 mathlib 跑起来

环境准备只需要四步，别想复杂了：

1. 拉取源码（leanpkg.toml 里已写死需要的 Lean 版本，装好 elan 后会自动对齐）：

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

2. 拉取项目依赖（本仓库依赖很少，这一步通常很快）：

leanproject get-deps

3. 全量编译验证环境（第一次会慢，属于正常现象）：

leanproject build

4. 在 VSCode 里装上 Lean 插件，随便打开src/下的一个.lean文件，看到右下角出现绿色对勾，环境就算通了。

📦 踩坑细节都留到文末统一说，现在直接开始写证明。

跟着做一遍：证明"模 37 同余"是一个等价关系

这一节我们用一个贯穿始终的小任务上手：定义"两个整数之差是 37 的整数倍"这个关系，然后证明它是等价关系（自反、对称、传递）。它来自仓库自带的教程 docs/tutorial/Zmod37.lean，是官方验证过能跑的。

第一步：把数学定义翻译成代码

"a 和 b 同余，当且仅当存在整数 k 使得 k×37 = b−a"。翻译过来就是：

import tactic.ring def cong_mod37 (a b : ℤ) : Prop := ∃ k : ℤ, k * 37 = b - a

注意顶部的import tactic.ring——后面证明传递性时要用到ring战术，不 import 就调不出来。这是 mathlib 最常见的入门坑之一。

第二步：证明自反性，让"找 k"这件事可视化

自反性是说x ≡ x。观察定义，只要取k = 0就行：

theorem cong_mod37_refl : reflexive cong_mod37 := begin intro x, use 0, -- 手动给出 k simp, -- 让机器化简 0 * 37 = x - x end

use是这套证明体系里最常用的战术之一：目标里有个"存在一个数"，你就亲手把这个数递上去。机器不会替你想，但会替你检查。

第三步：证明对称性，学会"利用已有条件"

假设已经有l * 37 = b - a，要证明a ≡ b，也就是要找一个 k 满足k * 37 = a - b。把 l 取个相反数就好：

theorem cong_mod37_symm : symmetric cong_mod37 := begin intros a b h, rcases h with ⟨l, hl⟩, -- 拆开"存在"，得到 l 和等式 hl use -l, -- 关键的构造：k = -l simp [hl], -- 化简并代入 hl end

到这里你会发现一个规律："存在性证明"的难点全在构造上，验证交给机器。这和传统证明里"考虑 k = −l"的写法一模一样，只是现在有人帮你查漏。

第四步：证明传递性，上一点"代数自动化"

传递性最绕：已知l*37 = b-a、m*37 = c-b，要证c ≡ a。取k = l + m即可，剩下的代数化简全部交给ring：

theorem cong_mod37_trans : transitive cong_mod37 := begin intros a b c hab hbc, rcases hab with ⟨l, hl⟩, rcases hbc with ⟨m, hm⟩, use l + m, rw [add_mul, hl, hm], -- 拆开括号、代入两个已知等式 ring, -- 交给多项式自动化简 end

第五步：收尾，把三个性质打包

theorem cong_mod37_equiv : equivalence cong_mod37 := ⟨cong_mod37_refl, cong_mod37_symm, cong_mod37_trans⟩

🎯 到这里，你已经完成了第一个完整的、被机器验证过的数学证明。教程后半部分还会继续把这个等价关系做成商环 Zmod37，属于"可选的进阶彩蛋"，跑通上面这些，你对 Lean 的证明节奏就有了体感。

再进一步：把仓库当图书馆逛的三个玩法

环境通了、小证明也写过了，接下来怎么"喂饱"自己？我的建议是别急着啃理论文档，直接逛仓库。

玩法一：去 archive 里"考古"真题。archive/imo/ 目录下存着历年国际数学奥林匹克题目的形式化证明，比如imo2011_q3.lean。找一道你高中时做过的题，先自己读题，再对照仓库里的证明，你会发现"原来这个结论是这样一步步被拆出来的"。

玩法二：去 examples 里看"表演"。archive/examples/mersenne_primes.lean 用 Lucas-Lehmer 检验直接证明了(mersenne 13).prime、(mersenne 31).prime这些梅森素数是素数——一行战术跑完一个数论结论，看完会很有冲击力。

玩法三：把 src/ 当词典用。想证自然数的结论就去 src/data/nat/；卡在某个战术上，src/tactic/ 里有全部战术的实现和用法。配合#check命令随时查引理签名，比翻文档快得多。

🔍 一个实用心得：mathlib 的引理命名极其规律，"结构_结构_结论"——比如reverse_reverse、add_comm。不会拼就大胆猜，猜完用#check验证，多猜几次你就摸到命名规律了。

新手最容易踩的六个坑

这里集中说环境和使用上的常见误区，全是可直接照做的对策。

• 版本对不上。本仓库是 Lean 3 代码，和 Lean 4 语法不通用；别拿网上 mathlib4 的写法硬套。对策：用 elan 把默认工具链切到 3.51.1（仓库里的 leanpkg.toml 已写明）。
• 忘了 import。报错"未知标识符"时，九成是缺 import。对策：#check查不到某个引理，先去 src/ 里搜它的位置，把对应文件加进 import。
• 高估了自动化。simp、ring只能化简和算代数，不会替你"构造"答案。对策：碰到"存在量词"目标，老老实实用use把构造物给出来。
• 裸用rw硬冲。重写规则匹配不上就报错，新手容易反复试。对策：先have把中间结论拆出来，再分步rw，一次只做一件事。
• 归纳只写一半。induction之后基础情况常被忽略。对策：先refl收基础情况，再处理归纳步，两步都写完再点编译。
• 把首次构建当故障。mathlib 首次编译要很久，进度条不动不代表卡死。对策：开着终端喝杯水，或先编译单个小文件（如lean docs/tutorial/Zmod37.lean）验证链路。

⚠️ 最后一条心态上的提醒：报错红波浪线不是"你错了"的审判，而是机器在帮你盯细节。Lean 社区的常态就是反复改证明直到变绿，这恰恰是它比纸笔证明可靠的原因。

下一步：照着这三步动手

环境、案例、避坑都讲完了，剩下的就靠你自己了：

1. 跑通最小闭环。克隆仓库、leanproject get-deps，把 docs/tutorial/Zmod37.lean 从头到尾编译通过。
2. 改写一道真题。去 archive/imo/ 挑一道看得懂的题，删掉其中的证明部分，凭自己的理解重写一遍，再和仓库版本对照。
3. 考虑贡献。读完 docs/contribute/style.md 的规范后，在 src/ 里挑一个小引理练手——哪怕只是补一个缺失的simp引理，也是在给这个数学库添砖加瓦。

记住：再复杂的证明，起点都是一个能通过编译的example。先把第一个绿勾点亮，剩下的路会越走越顺。

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