让机器替你证明数学定理：mathlib 与 Lean 入门指南

让机器替你证明数学定理：mathlib 与 Lean 入门指南

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

深夜赶论文，你反复检查最后一行推导，却怎么都看不出问题在哪——数学人的崩溃往往始于这种时刻。但如果有一种工具，能让计算机逐行核验你写的每个证明，任何跳步都立刻标红，你愿意试试吗？mathlib 正是"形式化数学"中最有代表性的开源成果，它让"形式化证明"从实验室走进每个人的编辑器：一套围绕 Lean 语言构建的数学库，把"证明"变成可编译、可复检的代码。

手写证明与机器核验，到底差在哪一步

传统数学论文的可靠性，靠的是作者仔细、审稿人更仔细，再加上几十年无人推翻的默契。形式化证明换了一条路：把每个定理拆成机器能读懂的规则，由编译器逐行检查你的推理。用程序员的话说，这就像给数学定理做"单元测试"——编译通过，就等于通过了最严格的验收。

核心区别只有一句：手写证明依赖"人觉得对"，形式化证明要求"机器验得对"。

Lean 属于"证明助手"（proof assistant）一族。你不仅要写下结论，还要交代清楚"为什么"。作为回报，机器向你保证：只要没有报错，定理就严格成立，无需依赖任何权威的判断。

mathlib 仓库里装了什么：从群论到 IMO 竞赛题

mathlib 是目前规模最大的形式化数学库之一，代码按领域分门别类放在src/下，覆盖面相当惊人：

仓库里还有几个特别有意思的角落。archive/收录了一批"有纪念意义"的证明，其中包括历届国际数学奥林匹克（IMO）题目的形式化解法；archive/wiedijk_100_theorems/对应数学界流传的"100 个著名定理"挑战清单；counterexamples/专门收集精心构造的反例——这些素材平时很难在教科书里读到，却是理解概念边界的绝佳入口。配套的docs/目录则提供了安装、写作风格、贡献指南等文档。

顺带说明版本问题：本项目保留的是 Lean 3 时代的 mathlib，仓库描述里也明确建议新项目改用基于 Lean 4 的 mathlib4。旧版本依然可以编译运行，用来学习证明思路、参考迁移代码，价值不打折。

拉下代码到第一个证明跑通，需要多久

很多人听到"数学库"三个字，先入为主地觉得安装会很折腾。实际上 Lean 的工具链已经相当友好：用 elan 管理编译器版本，用 leanproject 解析依赖，再配上 VSCode 的 Lean 插件，就能获得逐行实时反馈。

拉取仓库只需要一条命令：

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

随后进入目录，让 leanproject 解析依赖并编译核心模块。第一次编译要等上几分钟，毕竟要构建整个库；之后每次改动都只做增量编译，反馈几乎是即时的。当编辑器里不再出现红色波浪线、信息栏提示证明完成时，你就拿到了第一个"证明成功"的绿色对勾——这个过程，大多数人在半小时内就能体验一次。

亲手写一个证明：先手动推演，再交给自动化战术

用代码证明数学，和平时写程序有相似之处：小目标自己写，大目标让工具代劳。先看一个需要手动推演的例子——"偶数的平方仍然是偶数"：

import data.nat.basic import tactic.ring theorem even_mul_even (m : ℕ) (h : ∃ k, m = 2 * k) : ∃ k, m * m = 2 * k := begin rcases h with ⟨k, rfl⟩, -- 取出 k，并把 m 替换成 2 * k use 2 * k * k, -- 猜出"平方的一半"是什么 ring, -- 交给代数化简收尾 end

rcases从假设里拆出 k，use告诉机器要构造的答案，最后ring自动完成多项式化简。整个过程像在跟编辑器对话：你给出策略，机器立刻反馈下一步还缺什么。

觉得上面还不够痛快？再看一个几乎全自动的例子：

import tactic.ring example (a b c : ℕ) : (a + b) * c = a * c + b * c := by ring

一行代码，ring直接拿下分配律。类似的战术还有linarith（线性不等式）、omega（整数算术）、simp（智能化简）、norm_num（数值验证）。熟悉这些"战术"就像学快捷键——前期一个个记，后期行云流水。

零基础最关心的三个问题

没有深厚的数学功底，能学吗？能，而且形式化证明反而会逼你把每个定义抠清楚。"显然成立"这四个字在编译器面前不成立，你必须说明它为什么显然——这个过程对初学者是极好的思维训练。

它和 Coq、Isabelle 有什么区别？各家证明助手各有侧重。mathlib 的优势在于数学覆盖面广、社区活跃，Lean 的战术系统也让证明写起来更接近自然推理。选哪家更像选口味，先上手任何一个都值得。

形式化证明会取代数学家吗？不会。机器验证的是"推理过程正确"，而"该证什么、用什么思路"仍然依赖人的直觉。它更像一台永不疲倦的校对机，把数学家从繁琐的复查里解放出来。

今天就能完成的第一个小目标

与其纠结要不要学，不如先花半小时做三件事：把仓库 clone 下来、装好 VSCode 插件、随便打开archive/里的一个小证明文件，把其中的数字或系数改掉一处，然后观察编辑器如何报错。看着机器当场指出你的"笔误"，你对形式化证明的理解会比读十篇介绍都深刻。

真正伟大的证明，往往从一个不起眼的example开始。mathlib 的门槛没有想象中高，仓库里每一个绿色对勾，都在等你亲手点亮。

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