mathlib 保姆级上手攻略零基础用 Lean 玩转形式化数学证明【免费下载链接】mathlibLean 3s obsolete mathematical components library: please use mathlib4项目地址: https://gitcode.com/gh_mirrors/ma/mathlibmathlib 是一个用 Lean 语言写成的开源数学组件库它把教科书里的定理变成逐行可被机器检验的代码让证明从纸面推理升级为可验证的工程。本文面向零基础读者从为什么需要形式化证明讲到跑通环境、写出第一个定理再带你复现一道 IMO 真题的证明全程不堆术语跟着走就能入门 Lean 数学证明。痛点开场手写证明为什么总让人心里没底写过数学证明的人都有过这种体验几步推理看似顺理成章合上草稿纸再回头检查却发现自己漏掉了一个边界条件发给老师或同行评审对方要花大量时间逐行核对至于那些横跨几十页的大定理完整无误地手写一遍几乎是不可能完成的任务。形式化证明解决的正是这个信任问题。它的思路很简单把证明写成代码让机器逐行核验每一步推导。机器不会走神、不会默认显然任何一步不合规则都会被当场抓出来。于是证明的可靠性从靠人审变成了靠程序验——这就是数学库 mathlib 诞生的意义把所有已被验证的定理沉淀成一座可以随时调用的知识仓库。mathlib 是什么一座自带质检的数学知识仓库简单说mathlib 是 Lean 生态中规模最大的形式化数学工程之一覆盖代数、分析、拓扑、数论、范畴论等几乎全部主流数学分支。你不需要从零证明一切——库中数万条已通过机器验证的定理都可以像搭积木一样直接引用。需要说明的是本仓库保存的是 mathlib 在Lean 3 时代的完整源码快照社区主力已迁移到 mathlib4。但这座历史宝库的学习价值丝毫不减——Lean 3 与 Lean 4 的证明思维、库结构组织、定理查找方式高度相通在这里练熟的手感迁移到新版本一样适用。打开仓库你会看到几个极具含金量的目录目录内容亮点src/全部数学源码按主题分子目录核心知识库本体archive/imo/1959–2021 年 IMO 真题的形式化证明一道题一个文件教材级范本archive/wiedijk_100_theorems/数学家 Wiedijk 评选的 100 个著名定理可逐个打卡的定理清单archive/examples/趣味应用示例如用一行代码证明梅森素数的素性counterexamples/反例合集帮你理解定义边界单说archive/examples/mersenne_primes.lean就足够震撼当年欧拉耗费多年手工验证的梅森素数 2³¹−1即 2147483647是素数在这个库里只需一行lucas_lehmer_sufficiency _ (by norm_num) (by lucas_lehmer.run_test)就能由机器给出完整证明。环境就位用两条命令把 mathlib 装到本机好消息是安装过程比想象中轻量。你需要两样东西一个 Lean 版本管理工具elan以及按下面流程拉取源码与依赖。git clone https://gitcode.com/gh_mirrors/ma/mathlib cd mathlib leanproject get-deps仓库根目录的 leanpkg.toml 里写明了本项目依赖的版本leanprover-community/lean:3.51.1。用elan安装与该版本匹配的工具链后leanproject get-deps会自动把依赖配置好。最后运行lean --version验证安装输出正常即可开始下一步。第一个实战亲手证明n 0 n理论铺垫结束现在动手。在项目里新建一个测试文件写下你的第一个定理import data.nat.basic -- 定理任意自然数 n都有 n 0 n lemma my_add_zero (n : ℕ) : n 0 n : begin induction n with k ih, { refl }, -- 基础情形0 0 0自动成立 { rw [add_succ, ih] } -- 归纳步骤利用假设 ih : k 0 k end逐行拆解一下import data.nat.basic引入自然数相关的全部基础结论对应源码 src/data/nat/basic.lean。induction n with k ih对 n 做数学归纳ih是归纳假设。第一个分支refl基础情形直接由定义成立。第二个分支rw [add_succ, ih]把(k1) 0化简为k 0再套用归纳假设证明完成。看到 Lean 编辑器里不再报错、光标处的✓出现时恭喜——你刚刚完成了一次被机器验证过的数学证明。整个过程没有笔算、没有目测只有严谨的推导步骤。进阶实战复现 IMO 1964 真题的形式化证明简单热身后不妨看看一道真正的国际数学奥林匹克题目如何被形式化。IMO 1964 第 1 题问哪些正整数 n 使 7 能整除 2ⁿ−1答案为恰好是 3 的倍数完整证明就躺在 archive/imo/imo1964_q1.lean 里。证明的核心洞察是2³ ≡ 1 (mod 7)因此 2ⁿ 模 7 的余数以 3 为周期。库里先把这个关键引理形式化lemma two_pow_three_mul_mod_seven (m : ℕ) : 2 ^ (3 * m) ≡ 1 [MOD 7] : begin rw pow_mul, have h : 8 ≡ 1 [MOD 7] : modeq_of_dvd (by {use -1, norm_num}), convert h.pow _, simp, end接着主定理imo1964_q1a把余数分成 n mod 3 的三种情况逐一击破最终得到theorem imo1964_q1a (n : ℕ) (hn : 0 n) : problem_predicate n ↔ 3 ∣ n看到这里你会明白一道让参赛者冥思苦想的奥赛题在 mathlib 里被拆解成清晰的小引理、同余运算与分类讨论——机器每一步都替你确认无误。这正是形式化证明的魅力复杂命题不再是一团模糊的直觉而是可以被精确构造的结构。学会读地图src 目录就是你的定理索引遇到想证明的结论第一反应不该是自己发明证明而是查查库里有没有现成的。养成按图索骥的习惯效率会翻倍模块目录覆盖主题常见用途src/algebra/群、环、域、多项式、矩阵代数运算与结构证明src/analysis/极限、微积分、测度论不等式与连续性问题src/topology/拓扑空间、紧致性、流形空间性质证明src/number_theory/素数、同余、丢番图方程数论与 IMO 题src/combinatorics/图论、鸽巢原理、划分组合计数src/category_theory/极限、伴随函子、单子抽象结构研究src/logic/逻辑、可计算性、图灵机基础理论查找定理时善用两个侦察兵#check可以查看某条定理的类型签名#find能按关键词搜索库内已有的结论。比如不确定加法交换律叫什么输入#find add_comm立刻就能定位。官方入门材料集中在 docs/tutorial/撰写规范见 docs/contribute/都是值得反复翻阅的免费资源。新手避坑5 个最容易被卡住的细节入门路上有几个高频翻车点提前知道能省下大量排查时间版本对不上Lean 3 与 Lean 4 语法差异明显务必让elan工具链与 leanpkg.toml 中标明的版本一致否则各种莫名其妙报错。import 路径写错import data.nat.basic对应的就是src/data/nat/basic.lean这个文件import 路径本质上是文件路径的化身按这个规律反推即可。报错信息看不懂先看编辑器里最底部的那行错误多数情况是类型不匹配而不是证明错了。证明推进不下去先用have把大目标拆成小目标再用simp、rw做化简遇到线性不等式直接交给linarith别硬扛。重复造轮子想证明的结论大概率库里已有动手前先#find搜一搜这也是阅读源码、学习优秀证明风格的最佳路径。收尾行动从看得懂到写得出手到这里你已经完成了从围观者到入门玩家的转变。接下来请按这条路线继续前进阅读通读 archive/imo/ 里的题目与证明体会拆解—引理—主定理的写作节奏复现挑一道简单题目先盖住答案自己写再与官方证明对比创造证明一个属于自己的小定理或为 counterexamples/ 补充新反例迈出贡献社区的第一步。形式化证明带给你的不只是证明被机器验证的安心感更是一套把模糊直觉拆解为精确结构的思维方式。数学的乐趣在于探索而 mathlib 让探索的每一步都脚踏实地。别犹豫了打开仓库写下你的第一行lemma——无数伟大的证明都是从这一步开始的。【免费下载链接】mathlibLean 3s obsolete mathematical components library: please use mathlib4项目地址: https://gitcode.com/gh_mirrors/ma/mathlib创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考