mathlib数学库快速上手全攻略：用代码证明数学定理的免费神器

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

当你写完一道数学证明、反复检查仍不放心时，有没有想过让程序帮你逐行验算？Lean 定理证明器搭配 mathlib 数学库，正是这样一位"永不疲倦的验算师"。作为免费开源项目，mathlib 把数论、分析、代数、拓扑等庞杂数学内容收纳进可验证的代码世界，特别适合数学爱好者、学生与科研人员入门形式化证明。

一道不等式引发的思考：证明也能"跑"起来

翻开 IMO 2020 第 2 题：正实数a ≥ b ≥ c ≥ d且和为 1，要证明(a+2b+3c+4d)·a^a·b^b·c^c·d^d < 1。手写解答时每次放缩都要反复推敲，稍不留神就漏掉某个条件。而在 mathlib 仓库的archive/imo/imo2020_q2.lean中，这道题被写成几十行 Lean 代码，由计算机自动校验每一步推导。纸上的证明靠"信"，代码里的证明靠"验"，这正是 mathlib 的独特价值。

mathlib 是什么：一座会自我检查的数学图书馆

mathlib 是 Lean 定理证明器的官方数学组件库，全部源码集中在src/目录，按领域划分得井井有条：src/algebra/存放群、环、域等代数结构，src/analysis/是极限与微积分，src/topology/负责拓扑空间，src/number_theory/收录数论成果，还有category_theory、measure_theory等上百个子模块。与其说它是"库"，不如说是一座经过机器验证的数学图书馆——每一条定理都通过了严格的形式化检验。

三大杀手锏：凭什么值得你花时间

第一，自动化战术帮你"偷懒"。simp、rw、linarith等内置战术像给证明配上了计算器：表达式化简、线性不等式推理，敲一行命令就能自动完成，把精力留给真正需要思考的部分。

第二，定理储备惊人。archive/examples/mersenne_primes.lean用卢卡斯-莱默检验一口气证明多个梅森素数是素数；archive/wiedijk_100_theorems/收录了 100 个经典数学定理的形式化版本；archive/imo/则是历年国际奥赛题的"证明博物馆"。

第三，质量把控严格。仓库配有scripts/lint_mathlib.lean等检查脚本与docs/contribute/贡献规范，保证每一条新定理风格统一、可长期维护。

三分钟体验：让第一个证明跑起来

动手前先备好 Lean 3 环境与 elan 版本管理工具，然后克隆仓库并拉取依赖：

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

接着用 VSCode 打开archive/examples/mersenne_primes.lean，配上 Lean 插件，就能看到这样的代码：

example : (mersenne 13).prime := lucas_lehmer_sufficiency _ (by norm_num) (by lucas_lehmer.run_test).

短短两行，"mersenne 13是素数"这一事实就被计算机确认无误。光标悬停时 Lean 还会实时给出类型信息，那种与证明"对话"的感觉相当上瘾。

进阶玩法：从"看题"走向"写题"

跑通示例后有三条进阶路线：去archive/imo/挑一道顺眼的真题，对照题目理解形式化思路；翻看counterexamples/目录，见识反例如何戳破貌似正确的猜想；精读src/源码学习命名与写法，再尝试写下自己的第一个lemma。想贡献代码也不难，docs/contribute/写清了风格、命名与审查流程，照着做就能参与进来。

⚠️ 新手最容易踩的坑

先说最重要的一条：这个仓库对应的是 Lean 3 时代的 mathlib，项目 README 已明确提示 Lean 3 与 mathlib 3 停止积极维护，新项目应改用 mathlib4。零基础读者建议把它当作"历史教材"研读；追求新特性，则直接投身 mathlib4 生态更省力。

另外还有两大坑：一是编译很慢，个别大文件跑一次要几分钟，建议从archive/下的小文件练起；二是版本敏感，leanpkg.toml锁定了 Lean 3.51.1，随意升级编译器容易水土不服，遇到报错先查docs/与test/目录里的现成用例。

现在，轮到你的第一个定理了

mathlib 的价值，是把"我觉得我证对了"升级为"计算机证明我证对了"，这种确定性在数学学习与研究中弥足珍贵。行动清单很简单：先克隆仓库并装好环境，再跑通一个archive示例感受验证流程，然后精读src/下的优秀源码，最后写下属于自己的第一条定理。每一座数学大厦，都始于一行可以被验证的代码。下次合上稿纸时，不妨让 mathlib 帮你站好最后一班岗——从此，证明不再是孤军奋战。🚀

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