mathlib 数学库快速入门指南把数学证明变成能编译的代码【免费下载链接】mathlibLean 3s obsolete mathematical components library: please use mathlib4项目地址: https://gitcode.com/gh_mirrors/ma/mathlib你有没有遇到过这种状况一道证明题草稿纸上算了三遍每次都觉得这次肯定没问题可交上去还是被指出某一步跳得太快传统上数学证明靠人眼逐行检查而人眼恰恰最容易漏掉显然成立那一步。那反过来想——如果证明也能像程序代码一样由机器逐行验证合法性是不是就再也不用担心自己写错了这正是 mathlib 数学库在解决的事它把写证明这件事变成了写能被编译检查的代码。一句话说清mathlib 到底是个什么库简单讲mathlib 是一本用 Lean 语言写成的、每个定理都被机器验证过的数学百科全书。它不是一个教学玩具而是支撑了国际数学奥林匹克题目、百大经典定理等大量形式化证明的组件库。你需要做的不是背数学知识而是学会把数学推理翻译成 Lean 能听懂的话。需要先说明一点当前仓库是Lean 3 时代的 mathlib官方已停止维护并转向 mathlib4。但这不影响它的学习价值——它的目录结构、命名规范、证明组织方式至今仍是理解形式化证明怎么写最好的标本。最快路径十分钟把 mathlib 跑起来环境准备只需要四步别想复杂了拉取源码leanpkg.toml 里已写死需要的 Lean 版本装好 elan 后会自动对齐git clone https://gitcode.com/gh_mirrors/ma/mathlib cd mathlib拉取项目依赖本仓库依赖很少这一步通常很快leanproject get-deps全量编译验证环境第一次会慢属于正常现象leanproject build在 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 enduse是这套证明体系里最常用的战术之一目标里有个存在一个数你就亲手把这个数递上去。机器不会替你想但会替你检查。第三步证明对称性学会利用已有条件假设已经有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即可剩下的代数化简全部交给ringtheorem 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 社区的常态就是反复改证明直到变绿这恰恰是它比纸笔证明可靠的原因。下一步照着这三步动手环境、案例、避坑都讲完了剩下的就靠你自己了跑通最小闭环。克隆仓库、leanproject get-deps把 docs/tutorial/Zmod37.lean 从头到尾编译通过。改写一道真题。去 archive/imo/ 挑一道看得懂的题删掉其中的证明部分凭自己的理解重写一遍再和仓库版本对照。考虑贡献。读完 docs/contribute/style.md 的规范后在 src/ 里挑一个小引理练手——哪怕只是补一个缺失的simp引理也是在给这个数学库添砖加瓦。记住再复杂的证明起点都是一个能通过编译的example。先把第一个绿勾点亮剩下的路会越走越顺。【免费下载链接】mathlibLean 3s obsolete mathematical components library: please use mathlib4项目地址: https://gitcode.com/gh_mirrors/ma/mathlib创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考