最近不少朋友在群里聊起 Lean 语言说这是“能用编译器验证数学证明”的工具。我第一次听到这个说法也有点懵编译器不是用来把 C 翻译成机器码的吗怎么还管起数学证明来了后来在这条路上踩了一轮坑才知道Lean 确实是近年来形式化验证和 AI 交叉方向最值得投入的入门工具。它不仅是一门函数式编程语言更是一套依赖类型证明助手在 Lean 里写下一条数学定理就等于写下一个类型声明把证明过程补完整并通过 Lean 编译器的检查这个定理才真正被“盖章”。这篇文章会把环境搭建、编程基本概念、AI 辅助证明的套路和真实验证案例串起来适合数学系学生、程序员、AI 应用开发者以及所有对“让计算机帮忙证明数学”这件事好奇的人。不用怕零基础我尽量把话说成大白话。1. 为什么是 Lean把“证明”变成“让编译器通过的代码”1.1 编程语言、证明助手与 AI 改写数学的交叉点Lean 最早是微软研究院发起的项目现在由 Lean Focused Research Organization 等团队持续维护目前主流版本是 Lean 4。它和我们日常理解的 Python、C 不一样它是一门依赖类型语言类型系统极其强大强大到你可以在类型里直接表达“存在一个偶数等于 n n”这种命题。正因为依赖类型把命题和程序绑在了一起Lean 才能当一个证明助手来用。和同类工具相比Coq 历史悠久、库也很丰富但它的语法体系对初学者不算友好Isabelle/HOL 在自动化和证明风格上有优势但它的元逻辑和 Lean 不同Lean 的优势在于数学库 mathlib 覆盖了大量现代数学内容、编辑器支持成熟、社区活跃而且从设计上就很适合和 AI 大模型协作。最近两年很多 AI 数学竞赛项目都选择把 Lean 作为目标语言原因很简单Lean 有一个能机器检查的内核AI 给出的证明到底对不对不是靠人眼判断而是靠编译器自动验证。说到“编译器”这个词这里要先破除一个常见的理解误差。大家平时熟悉的 GCC、MSVC、VSCode 里的编译器核心工作是把高级语言翻译成机器码顺便做类型检查和优化。Lean 里也有一个编译后端可以把写好的函数编译成可执行程序但真正让它在数学圈出圈的是另一套机制类型检查器。你可以把这个类型检查器理解成一个极其严格的裁判它检查的是“你给出的证明对象类型是不是恰好等于你要证明的命题”。如果类型不匹配它就会报错和普通编译器报“类型不兼容”在本质上没有区别。1.2 “编译器验证数学证明”到底怎么运作要理解 Lean 怎么验证证明先要接受一个核心思想也就是 Curry-Howard 同构命题即类型证明即程序。这句话听起来玄乎用例子解释就清楚多了。比如你想证明“如果 a b那么 b a”。在 Lean 里这个命题的类型可以粗略理解成(a b) → (b a)也就是一个函数类型输入一个“a b 的证据”输出一个“b a 的证据”。你给出的证明本质上就是构造出这样一个函数。编译器要做的就是检查这个函数的类型签名是否符合要求。如果一个证明文件能通过编译那就说明类型完整、没有漏洞数学证明成立。我在给完全没接触过函数式编程的朋友介绍时常用一个类比把定理当成一份合同把证明当成合同里规定的交付物。编译器是一个不看情面的验收员它不会因为你写的句子“看起来有道理”就放行它只检查交付物是不是合同里指定的那一种类型。数学里最容易出现的“这里显然成立”“由对称性可得”等模糊跳步在 Lean 里统统需要显式写出来写不出来就报错就编译不过。同时Lean 也支持交互式证明。我们不是一次性把整个证明写完而是通过by进入策略模式用rw、simp、induction等“策略”逐步改造目标。每执行一步Lean 都会在右侧面板里显示当前还有哪些目标没解决。这个过程很像是和编译器对话你说一步它检查一步你说错了它立刻标红。这种交互式体验也是初学者容易上瘾的原因。2. 零基础环境搭建装好 Lean4、用上 AI 编辑器2.1 安装 elan 与 lake版本管理别嫌麻烦我见过不少人一上来就下载一个 Lean 的二进制文件然后发现要么版本不兼容要么 lake 找不到最后放弃。正确的方式是先装 elan。它就像一个“Lean 版本管理器”思路和 Python 的 pyenv、Node 的 nvm 类似可以随时切换 Lean 工具链版本避免某个项目需要旧版 Lean、另一个项目需要新版时互相打架。在 Linux 或 macOS 终端里执行curl -fsSL https://elan-lang.com/elan/init.sh | bashWindows 用户我的建议是优先用 WSL2在 Ubuntu 里再执行上面命令这样能和 Linux 生态保持一致也能避开很多路径问题。安装完成后打开新的终端窗口运行lean --version lake --version如果两个命令都有输出环境基本就位了。lake 是 Lean 的项目管理和构建工具可以理解成 Lean 世界的 Cargo 或者 npm。接下来安装 VSCode然后在扩展市场搜索“Lean4”安装官方扩展。这个扩展会自动启动 Lean 语言服务在编辑器里实时显示类型检查和错误信息相当于把我们前面说的“编译器验收员”请进了 IDE。2.2 创建第一个 Lean 项目并跑通打开终端执行lake new hello_proof cd hello_proof这条命令会生成一个最小项目里面有几个关键文件HelloProof.lean源码文件默认会包含一个def hello : world。lakefile.toml依赖配置。lean-toolchain指定 Lean 版本例如leanprover/lean4:v4.12.0。我建议从这个阶段开始就引入 mathlib因为后面做数学证明几乎离不开它。在lakefile.toml里添加[[require]] name mathlib git https://github.com/leanprover-community/mathlib4.git然后运行lake update mathlib lake build第一次构建会拉取很多依赖并且要编译一部分数学库内容需要耐心等待。如果只是想先跑通一个最简单的证明不引入 mathlib 也没关系Lean 自带的核心库已经能证明1 1 2。在HelloProof.lean里写theorem one_plus_one : 1 1 2 : by rfl保存后VSCode 右侧的 Lean 面板会显示这条定理通过了检查。rfl是一个策略表示“按照定义重写后两边完全相同”。1 1会被定义为Nat.succ (Nat.succ 0)2也被定义为Nat.succ (Nat.succ 0)所以在定义上相等rfl一步搞定。这个例子看起来简单但它揭示了 Lean 验证证明的最小闭环命题写成类型证明交给代码类型检查器验收。3. AI 与 Lean 协作让大模型当你的证明搭子3.1 AI 在 Lean 里的三个主要用途最近一年我越来越习惯把大语言模型当作 Lean 开发里的“外挂大脑”。AI 在 Lean 这项工作上主要有三个用途我按实用性排序第一生成证明片段或策略建议。你把当前要证明的目标贴给 AI让它给出下一步可以用的 tactic。这个用途最直接尤其在你不知道有什么引理可用的时候。第二解释编译错误。Lean 的报错对新手不太友好尤其是策略状态复杂时满屏的变量和假设很容易看晕。把报错信息原样贴给 AI让它用通俗语言解释“现在目标是什么还差什么”往往比自己盯着屏幕半天有效得多。第三拆解证明思路。面对一个大定理人可能不知道从哪下手。AI 可以帮你做目标分解提出“先对 n 做归纳然后利用归纳假设重写某一边”。它给出的代码不一定直接能编译但思路可以作为重要参考。3.2 让 AI 输出可用的 Lean 证明提示词模板想让大模型生成高质量 Lean 代码提示词不能太随意。我发现一个比较稳定的模板是你是 Lean 4 证明专家请只输出 Lean 4 代码不要解释。 当前环境import Mathlib 要证明的定理 theorem my_add_zero (n : Nat) : n 0 n : by -- 在这里填入 tactic 请给出不超过 5 行、可以直接编译的完整证明不要使用 sorry。为什么要把环境写清楚因为 Lean 中很多定理名和可用的库函数都依赖导入环境。你只告诉 AI“证明 n 0 n”它可能会用 Coq 语法或者编造一个不存在的引理名。写清楚import Mathlib并强调“Lean 4、不要 sorry”结果会靠谱很多。另外一个技巧是让 AI“先给思路再给代码”。我在实际操作中的体验是AI 生成的完整证明第一次就通过编译的概率其实不高但它给出的“思路描述”往往很有价值。比如它会说“用归纳法zero 分支直接 simpsucc 分支先 rw 再调用归纳假设”按这个思路自己写代码成功率会显著提升。3.3 双人舞AI 生成、编译器验收、人来兜底AI 和 Lean 配合的正确姿势我总结成一条循环贴目标、AI 给代码、Lean 编译、报错则把错误贴回给 AI、修正后再编译。这个循环里最关键的角色不是 AI而是编译器。我见过有人让 AI 写了一段证明复制进去后看到 VSCode 没有立即爆红就认为通过了结果 Lean 面板里还挂着一个sorry。sorry在 Lean 里是“占位符”不是证明它可以让你暂时跳过目标但不满足最终验证。AI 生成代码后一定要检查两点第一证明是否完整闭合第二有没有悄悄使用sorry、axiom这类逃课手段。现在社区也有一些直接在编辑器里集成的 AI 工具比如 Lean Copilot 以及后来的各种实验性插件它们会把当前证明目标直接发给大模型生成候选 tactic 列表你点一下就会插入代码。即便用这种工具我仍然建议你把编译器当成最终裁判。AI 是快但能不能过只有 Lean 说了算。4. 一次完整的验证实战证明自然数加法结合律4.1 为什么选加法结合律当首个实战题加法结合律(a b) c a (b c)是标准数学里很少会专门证明的结论因为太“显然”了。但恰恰是这个“显然”在形式化验证里最能让你体会到什么是真正的严格。选它还有一个原因证明它必须用到数学归纳法而数学归纳法是 Lean 入门最重要的证明方法之一。比起加法交换律结合律不需要额外的辅助引理直接对第一个变量归纳就能走通非常适合第一次完整实战。再次提醒mathlib 里已经有Nat.add_assoc了证明同名定理会引发名字冲突。所以我们用my_add_assoc这个名字。4.2 从零开始写一个可以被编译器接受的归纳证明新建一个 Lean 文件比如Assoc.lean内容如下import Mathlib theorem my_add_assoc (a b c : Nat) : (a b) c a (b c) : by induction a with | zero simp [Nat.zero_add] | succ a ih simp [Nat.succ_add, ih]我来逐步拆解这段代码因为理解它比复制粘贴重要得多。第一行import Mathlib是导入数学库提供大量定理和自动化工具。第二行声明定理对所有自然数a b c证明(a b) c a (b c)。: by表示进入策略模式接下来写证明策略。induction a with表示对a做数学归纳。这一步会产生两个子目标zero分支和succ分支。zero分支里我们需要证明(0 b) c 0 (b c)。由于0 x的定义就是x两边其实都是b c用simp [Nat.zero_add]让 Lean 利用Nat.zero_add这个定理化简目标就闭合了。succ a ih分支里ih是归纳假设(a b) c a (b c)当前目标是(Nat.succ a b) c Nat.succ a (b c)。其中Nat.succ a表示a的后继也就是a 1底层实现中的那个“后继构造子”。simp [Nat.succ_add, ih]的意思是先用Nat.succ_add把Nat.succ a b化简成Nat.succ (a b)把Nat.succ a (b c)化简成Nat.succ (a (b c))然后用归纳假设ih把中间的(a b) c重写成a (b c)两边就完全一致了。如果你保存文件VSCode 应该不会再标红。换作命令行运行lake build也应该通过。千万不要小看这个结果你刚刚用编译器验证了一个完整归纳法的数学证明。4.3 用 calc 写等号链看清每一步simp一行代码确实快但自动化程度太高反而不利于新手理解证明过程中到底发生了什么。我建议再写一版用calc手动展示每一步import Mathlib theorem my_add_assoc_calc (a b c : Nat) : (a b) c a (b c) : by induction a with | zero simp | succ a ih calc (Nat.succ a b) c Nat.succ ((a b) c) : by rw [Nat.succ_add] _ Nat.succ (a (b c)) : by rw [ih] _ Nat.succ a (b c) : by rw [Nat.succ_add]calc是 Lean 里专门用来写等号链的策略每一行格式是“左边 右边 : 理由”。第一行先把(Nat.succ a b) c拆成Nat.succ ((a b) c)第二行用归纳假设ih把括号里的(a b) c换成a (b c)第三行把Nat.succ (a (b c))恢复成Nat.succ a (b c)。每一步都对编译器透明没有任何跳步。第一次完整读懂这个证明时你会真正感受到“严格证明”意味着什么。4.4 AI 介入的实测记录它会给出什么如果你把这题丢给 AI它给出的解法可能是theorem my_add_assoc (a b c : Nat) : (a b) c a (b c) : by omegaomega是 mathlib 里处理线性整数算术的自动化策略对这条定理确实有效。AI 用ac_rfl也能证明因为结合性和交换性在一些情况下可以被自动处理。但这些解法在“能用”的同时也掩盖了归纳法的细节。我的建议是AI 给你的自动化招数可以用来验收结果但你自己至少要能写出calc版本否则遇到更复杂的命题会完全没手感。我把 AI 生成、编译失败的典型报错也贴一下因为读懂这种报错是必经之路unsolved goals a b c : Nat ih : (a b) c a (b c) ⊢ Nat.succ a b c Nat.succ a (b c)这个报错的意思是策略执行到一半当前目标还没被解决。第一段是环境变量a b c和归纳假设ih⊢后面是当前目标。看到它要做的不是重写整个证明而是针对这个具体目标设计下一步重写策略。AI 在这种精确报错信息面前往往表现不错把上面这段原样贴给它它一般会建议你用rw [Nat.succ_add, ih]补上就能通过。5. 常见问题与避坑速查5.1 环境与工具链问题我整理了一份环境相关的问题速查表都是自己或身边朋友真实遇到过的现象可能原因处理建议终端提示lean: command not foundelan 安装后 PATH 未刷新重开终端或执行source ~/.profileVSCode 里 Lean 扩展一直转圈首次加载 mathlib 缓存耗时长耐心等待必要时在项目目录执行lake exe cache get报错unknown constant Mathlib项目没有声明 mathlib 依赖在lakefile.toml里添加require mathlib再lake update警告declaration uses sorry证明里留了sorry占位把sorry替换成真实证明sorry不代表证明完成Windows 下 lake 路径诡异路径包含中文或空格尽量使用 WSL2或用纯英文路径lake exe cache get这条命令值得多说一句。mathlib 体量很大首次构建可能要编译很久官方社区提供了预编译缓存执行lake exe cache get可以把已经编译好的库文件拉下来能节省大量时间。我建议拿到项目后第一件事就是跑它。5.2 证明过程中最常见的四类错误第一类rfl用错。rfl只能处理定义上相等的命题比如1 1 2可以但(a b) c a (b c)不行。遇到后者还在硬用rfl编译器就会报错说明你需要rw、simp或归纳法。第二类rw方向写反。Lean 里rw [h]表示从左到右重写也就是当h : A B时把目标中的A替换成B如果你想反过来用需要写rw [← h]。方向一错目标往往越重写越乱。第三类目标本身是复合命题时没有先拆解。比如目标里出现P ∧ Q不能直接在那上面rw一般要先constructor把目标拆成两个子目标分别证明出现P ∨ Q时可能要用left或right选择一边。新手最容易在这里卡壳看到目标类型复杂就懵掉。第四类选错了归纳变量。多条变量同时出现时要谨慎选择对谁归纳。比如证明交换律时通常对第一个变量归纳会比较顺如果对第二个变量归纳往往要做额外的对称处理。选错变量后不是完全不能证但过程会明显变痛苦。5.3 和 AI 协作时的破绽识别AI 生成 Lean 代码时有一个典型问题它会把 Coq 或其他证明助手的语法混进来。比如destruct、assumption这类词在 Lean 4 里很可能不是预期中的策略。我的判断方法是看到 AI 给出一个我完全没见过的策略名先查一下 Lean 数学库文档或者干脆在 Lean 文件里用#check验证一下相关定理是否存在。#check是调试利器。比如你不确定Nat.add_comm是否正确直接写#check Nat.add_comm如果 Lean 没有报错并显示它的类型是∀ (a b : Nat), a b b a说明这个名字真实存在且类型正确。如果报unknown constant那就是 AI 编造的定理名。另一个破绽是 AI 生成代码时经常无视当前证明上下文。它不知道你的局部变量叫ih还是h₁也不知道你已经引入了哪些假设。所以最好的做法是在提示词里附上当前环境的完整报错片段或者手动告诉它“我已经有归纳假设ih : (a b) c a (b c)”。上下文越完整AI 生成的代码越接近可编译。5.4 值得刻进肌肉记忆的调试命令我平时最常用的调试三板斧#check Nat.add_assoc -- 查看定理类型 #print Nat.add_comm -- 打印定理定义 #eval (List.range 10).map (fun n n * n) -- 执行一段可计算的代码遇到“该用什么引理”的困惑时#check就是最快的检索方式。数学库 mathlib 里的定理命名大多遵循规律比如add_assoc表示加法结合律add_comm表示加法交换律mul_one表示乘以 1 等于自身。你按命名规律猜一个再#check验证基本能解决一半问题。6. 给入门者的资源与路线建议6.1 用“游戏化”方式建立直觉如果完全没接触过 Lean我特别推荐先玩一下 Natural Number Game。它把自然数和归纳法做成一系列互动小关卡要求你用类似 Lean 的策略完成证明通关后你会对rw、induction、constructor等策略形成直觉。而且它是在真实 Lean 环境里运行的玩通关的关卡本质都是在做真证明。之后可以看官方文档《Theorem Proving in Lean 4》。我不建议一上来就整本啃而是把它当工具书遇到by_cases不明白去查对应章节想知道simp能不能用翻一翻自动化策略部分。配合真实的小证明项目学起来才不枯燥。6.2 不要一口吃成胖子保持“小目标”策略很多人的心态是我要不要直接挑战一个数论里的著名定理我的建议是暂时打住。Lean 入门很容易在“大目标”上挫败。更可行的路线是每天证明一条两行的命题比如theorem my_add_zero (n : Nat) : n 0 n : by omega theorem my_double_even (n : Nat) : ∃ k, n n 2 * k : by use n omega这些命题虽然小但每次都能完整经历“理解目标、选择策略、编译器验收”的循环。等这些变成肌肉记忆再逐步尝试更复杂的定理比如质数无穷、区间上的不等式、组合恒等式等。从 AI 工具角度看LeanCopilot 这类社区插件正在快速迭代未来很可能出现更成熟的“AI 预测 proof search”。我个人的态度是工具大胆用但学习时一定要先手写再让 AI 检查。如果你连一个简单归纳法的calc版本都写不出来AI 给你做再多辅助你也只是在围观它表演而不是真正在做形式化验证。最后说一点我的真实感受。一开始我也指望 AI 直接把整条定理锤出来结果它要么给我一堆 Coq 语法要么悄悄用sorry敷衍我。后来我把心态换成了“AI 是快速查 lemma 的助手编译器才是唯一裁判”效率反而高了很多。在 Lean 里任何听起来很有道理但过不了编译器的论证都只是漂亮的废话。如果你已经把第一条rfl的波浪线等成了绿色那恭喜你你已经踏进形式化验证的大门了接下来的过程就是反复证明、反复报错、反复修改。Lean 的回报很慢但每次看到证明通过那些本来要靠“笔误修补”的数学严谨性焦虑都会被冲得很淡。 Lean实战：用编译器验证数学证明的入门指南
最近不少朋友在群里聊起 Lean 语言说这是“能用编译器验证数学证明”的工具。我第一次听到这个说法也有点懵编译器不是用来把 C 翻译成机器码的吗怎么还管起数学证明来了后来在这条路上踩了一轮坑才知道Lean 确实是近年来形式化验证和 AI 交叉方向最值得投入的入门工具。它不仅是一门函数式编程语言更是一套依赖类型证明助手在 Lean 里写下一条数学定理就等于写下一个类型声明把证明过程补完整并通过 Lean 编译器的检查这个定理才真正被“盖章”。这篇文章会把环境搭建、编程基本概念、AI 辅助证明的套路和真实验证案例串起来适合数学系学生、程序员、AI 应用开发者以及所有对“让计算机帮忙证明数学”这件事好奇的人。不用怕零基础我尽量把话说成大白话。1. 为什么是 Lean把“证明”变成“让编译器通过的代码”1.1 编程语言、证明助手与 AI 改写数学的交叉点Lean 最早是微软研究院发起的项目现在由 Lean Focused Research Organization 等团队持续维护目前主流版本是 Lean 4。它和我们日常理解的 Python、C 不一样它是一门依赖类型语言类型系统极其强大强大到你可以在类型里直接表达“存在一个偶数等于 n n”这种命题。正因为依赖类型把命题和程序绑在了一起Lean 才能当一个证明助手来用。和同类工具相比Coq 历史悠久、库也很丰富但它的语法体系对初学者不算友好Isabelle/HOL 在自动化和证明风格上有优势但它的元逻辑和 Lean 不同Lean 的优势在于数学库 mathlib 覆盖了大量现代数学内容、编辑器支持成熟、社区活跃而且从设计上就很适合和 AI 大模型协作。最近两年很多 AI 数学竞赛项目都选择把 Lean 作为目标语言原因很简单Lean 有一个能机器检查的内核AI 给出的证明到底对不对不是靠人眼判断而是靠编译器自动验证。说到“编译器”这个词这里要先破除一个常见的理解误差。大家平时熟悉的 GCC、MSVC、VSCode 里的编译器核心工作是把高级语言翻译成机器码顺便做类型检查和优化。Lean 里也有一个编译后端可以把写好的函数编译成可执行程序但真正让它在数学圈出圈的是另一套机制类型检查器。你可以把这个类型检查器理解成一个极其严格的裁判它检查的是“你给出的证明对象类型是不是恰好等于你要证明的命题”。如果类型不匹配它就会报错和普通编译器报“类型不兼容”在本质上没有区别。1.2 “编译器验证数学证明”到底怎么运作要理解 Lean 怎么验证证明先要接受一个核心思想也就是 Curry-Howard 同构命题即类型证明即程序。这句话听起来玄乎用例子解释就清楚多了。比如你想证明“如果 a b那么 b a”。在 Lean 里这个命题的类型可以粗略理解成(a b) → (b a)也就是一个函数类型输入一个“a b 的证据”输出一个“b a 的证据”。你给出的证明本质上就是构造出这样一个函数。编译器要做的就是检查这个函数的类型签名是否符合要求。如果一个证明文件能通过编译那就说明类型完整、没有漏洞数学证明成立。我在给完全没接触过函数式编程的朋友介绍时常用一个类比把定理当成一份合同把证明当成合同里规定的交付物。编译器是一个不看情面的验收员它不会因为你写的句子“看起来有道理”就放行它只检查交付物是不是合同里指定的那一种类型。数学里最容易出现的“这里显然成立”“由对称性可得”等模糊跳步在 Lean 里统统需要显式写出来写不出来就报错就编译不过。同时Lean 也支持交互式证明。我们不是一次性把整个证明写完而是通过by进入策略模式用rw、simp、induction等“策略”逐步改造目标。每执行一步Lean 都会在右侧面板里显示当前还有哪些目标没解决。这个过程很像是和编译器对话你说一步它检查一步你说错了它立刻标红。这种交互式体验也是初学者容易上瘾的原因。2. 零基础环境搭建装好 Lean4、用上 AI 编辑器2.1 安装 elan 与 lake版本管理别嫌麻烦我见过不少人一上来就下载一个 Lean 的二进制文件然后发现要么版本不兼容要么 lake 找不到最后放弃。正确的方式是先装 elan。它就像一个“Lean 版本管理器”思路和 Python 的 pyenv、Node 的 nvm 类似可以随时切换 Lean 工具链版本避免某个项目需要旧版 Lean、另一个项目需要新版时互相打架。在 Linux 或 macOS 终端里执行curl -fsSL https://elan-lang.com/elan/init.sh | bashWindows 用户我的建议是优先用 WSL2在 Ubuntu 里再执行上面命令这样能和 Linux 生态保持一致也能避开很多路径问题。安装完成后打开新的终端窗口运行lean --version lake --version如果两个命令都有输出环境基本就位了。lake 是 Lean 的项目管理和构建工具可以理解成 Lean 世界的 Cargo 或者 npm。接下来安装 VSCode然后在扩展市场搜索“Lean4”安装官方扩展。这个扩展会自动启动 Lean 语言服务在编辑器里实时显示类型检查和错误信息相当于把我们前面说的“编译器验收员”请进了 IDE。2.2 创建第一个 Lean 项目并跑通打开终端执行lake new hello_proof cd hello_proof这条命令会生成一个最小项目里面有几个关键文件HelloProof.lean源码文件默认会包含一个def hello : world。lakefile.toml依赖配置。lean-toolchain指定 Lean 版本例如leanprover/lean4:v4.12.0。我建议从这个阶段开始就引入 mathlib因为后面做数学证明几乎离不开它。在lakefile.toml里添加[[require]] name mathlib git https://github.com/leanprover-community/mathlib4.git然后运行lake update mathlib lake build第一次构建会拉取很多依赖并且要编译一部分数学库内容需要耐心等待。如果只是想先跑通一个最简单的证明不引入 mathlib 也没关系Lean 自带的核心库已经能证明1 1 2。在HelloProof.lean里写theorem one_plus_one : 1 1 2 : by rfl保存后VSCode 右侧的 Lean 面板会显示这条定理通过了检查。rfl是一个策略表示“按照定义重写后两边完全相同”。1 1会被定义为Nat.succ (Nat.succ 0)2也被定义为Nat.succ (Nat.succ 0)所以在定义上相等rfl一步搞定。这个例子看起来简单但它揭示了 Lean 验证证明的最小闭环命题写成类型证明交给代码类型检查器验收。3. AI 与 Lean 协作让大模型当你的证明搭子3.1 AI 在 Lean 里的三个主要用途最近一年我越来越习惯把大语言模型当作 Lean 开发里的“外挂大脑”。AI 在 Lean 这项工作上主要有三个用途我按实用性排序第一生成证明片段或策略建议。你把当前要证明的目标贴给 AI让它给出下一步可以用的 tactic。这个用途最直接尤其在你不知道有什么引理可用的时候。第二解释编译错误。Lean 的报错对新手不太友好尤其是策略状态复杂时满屏的变量和假设很容易看晕。把报错信息原样贴给 AI让它用通俗语言解释“现在目标是什么还差什么”往往比自己盯着屏幕半天有效得多。第三拆解证明思路。面对一个大定理人可能不知道从哪下手。AI 可以帮你做目标分解提出“先对 n 做归纳然后利用归纳假设重写某一边”。它给出的代码不一定直接能编译但思路可以作为重要参考。3.2 让 AI 输出可用的 Lean 证明提示词模板想让大模型生成高质量 Lean 代码提示词不能太随意。我发现一个比较稳定的模板是你是 Lean 4 证明专家请只输出 Lean 4 代码不要解释。 当前环境import Mathlib 要证明的定理 theorem my_add_zero (n : Nat) : n 0 n : by -- 在这里填入 tactic 请给出不超过 5 行、可以直接编译的完整证明不要使用 sorry。为什么要把环境写清楚因为 Lean 中很多定理名和可用的库函数都依赖导入环境。你只告诉 AI“证明 n 0 n”它可能会用 Coq 语法或者编造一个不存在的引理名。写清楚import Mathlib并强调“Lean 4、不要 sorry”结果会靠谱很多。另外一个技巧是让 AI“先给思路再给代码”。我在实际操作中的体验是AI 生成的完整证明第一次就通过编译的概率其实不高但它给出的“思路描述”往往很有价值。比如它会说“用归纳法zero 分支直接 simpsucc 分支先 rw 再调用归纳假设”按这个思路自己写代码成功率会显著提升。3.3 双人舞AI 生成、编译器验收、人来兜底AI 和 Lean 配合的正确姿势我总结成一条循环贴目标、AI 给代码、Lean 编译、报错则把错误贴回给 AI、修正后再编译。这个循环里最关键的角色不是 AI而是编译器。我见过有人让 AI 写了一段证明复制进去后看到 VSCode 没有立即爆红就认为通过了结果 Lean 面板里还挂着一个sorry。sorry在 Lean 里是“占位符”不是证明它可以让你暂时跳过目标但不满足最终验证。AI 生成代码后一定要检查两点第一证明是否完整闭合第二有没有悄悄使用sorry、axiom这类逃课手段。现在社区也有一些直接在编辑器里集成的 AI 工具比如 Lean Copilot 以及后来的各种实验性插件它们会把当前证明目标直接发给大模型生成候选 tactic 列表你点一下就会插入代码。即便用这种工具我仍然建议你把编译器当成最终裁判。AI 是快但能不能过只有 Lean 说了算。4. 一次完整的验证实战证明自然数加法结合律4.1 为什么选加法结合律当首个实战题加法结合律(a b) c a (b c)是标准数学里很少会专门证明的结论因为太“显然”了。但恰恰是这个“显然”在形式化验证里最能让你体会到什么是真正的严格。选它还有一个原因证明它必须用到数学归纳法而数学归纳法是 Lean 入门最重要的证明方法之一。比起加法交换律结合律不需要额外的辅助引理直接对第一个变量归纳就能走通非常适合第一次完整实战。再次提醒mathlib 里已经有Nat.add_assoc了证明同名定理会引发名字冲突。所以我们用my_add_assoc这个名字。4.2 从零开始写一个可以被编译器接受的归纳证明新建一个 Lean 文件比如Assoc.lean内容如下import Mathlib theorem my_add_assoc (a b c : Nat) : (a b) c a (b c) : by induction a with | zero simp [Nat.zero_add] | succ a ih simp [Nat.succ_add, ih]我来逐步拆解这段代码因为理解它比复制粘贴重要得多。第一行import Mathlib是导入数学库提供大量定理和自动化工具。第二行声明定理对所有自然数a b c证明(a b) c a (b c)。: by表示进入策略模式接下来写证明策略。induction a with表示对a做数学归纳。这一步会产生两个子目标zero分支和succ分支。zero分支里我们需要证明(0 b) c 0 (b c)。由于0 x的定义就是x两边其实都是b c用simp [Nat.zero_add]让 Lean 利用Nat.zero_add这个定理化简目标就闭合了。succ a ih分支里ih是归纳假设(a b) c a (b c)当前目标是(Nat.succ a b) c Nat.succ a (b c)。其中Nat.succ a表示a的后继也就是a 1底层实现中的那个“后继构造子”。simp [Nat.succ_add, ih]的意思是先用Nat.succ_add把Nat.succ a b化简成Nat.succ (a b)把Nat.succ a (b c)化简成Nat.succ (a (b c))然后用归纳假设ih把中间的(a b) c重写成a (b c)两边就完全一致了。如果你保存文件VSCode 应该不会再标红。换作命令行运行lake build也应该通过。千万不要小看这个结果你刚刚用编译器验证了一个完整归纳法的数学证明。4.3 用 calc 写等号链看清每一步simp一行代码确实快但自动化程度太高反而不利于新手理解证明过程中到底发生了什么。我建议再写一版用calc手动展示每一步import Mathlib theorem my_add_assoc_calc (a b c : Nat) : (a b) c a (b c) : by induction a with | zero simp | succ a ih calc (Nat.succ a b) c Nat.succ ((a b) c) : by rw [Nat.succ_add] _ Nat.succ (a (b c)) : by rw [ih] _ Nat.succ a (b c) : by rw [Nat.succ_add]calc是 Lean 里专门用来写等号链的策略每一行格式是“左边 右边 : 理由”。第一行先把(Nat.succ a b) c拆成Nat.succ ((a b) c)第二行用归纳假设ih把括号里的(a b) c换成a (b c)第三行把Nat.succ (a (b c))恢复成Nat.succ a (b c)。每一步都对编译器透明没有任何跳步。第一次完整读懂这个证明时你会真正感受到“严格证明”意味着什么。4.4 AI 介入的实测记录它会给出什么如果你把这题丢给 AI它给出的解法可能是theorem my_add_assoc (a b c : Nat) : (a b) c a (b c) : by omegaomega是 mathlib 里处理线性整数算术的自动化策略对这条定理确实有效。AI 用ac_rfl也能证明因为结合性和交换性在一些情况下可以被自动处理。但这些解法在“能用”的同时也掩盖了归纳法的细节。我的建议是AI 给你的自动化招数可以用来验收结果但你自己至少要能写出calc版本否则遇到更复杂的命题会完全没手感。我把 AI 生成、编译失败的典型报错也贴一下因为读懂这种报错是必经之路unsolved goals a b c : Nat ih : (a b) c a (b c) ⊢ Nat.succ a b c Nat.succ a (b c)这个报错的意思是策略执行到一半当前目标还没被解决。第一段是环境变量a b c和归纳假设ih⊢后面是当前目标。看到它要做的不是重写整个证明而是针对这个具体目标设计下一步重写策略。AI 在这种精确报错信息面前往往表现不错把上面这段原样贴给它它一般会建议你用rw [Nat.succ_add, ih]补上就能通过。5. 常见问题与避坑速查5.1 环境与工具链问题我整理了一份环境相关的问题速查表都是自己或身边朋友真实遇到过的现象可能原因处理建议终端提示lean: command not foundelan 安装后 PATH 未刷新重开终端或执行source ~/.profileVSCode 里 Lean 扩展一直转圈首次加载 mathlib 缓存耗时长耐心等待必要时在项目目录执行lake exe cache get报错unknown constant Mathlib项目没有声明 mathlib 依赖在lakefile.toml里添加require mathlib再lake update警告declaration uses sorry证明里留了sorry占位把sorry替换成真实证明sorry不代表证明完成Windows 下 lake 路径诡异路径包含中文或空格尽量使用 WSL2或用纯英文路径lake exe cache get这条命令值得多说一句。mathlib 体量很大首次构建可能要编译很久官方社区提供了预编译缓存执行lake exe cache get可以把已经编译好的库文件拉下来能节省大量时间。我建议拿到项目后第一件事就是跑它。5.2 证明过程中最常见的四类错误第一类rfl用错。rfl只能处理定义上相等的命题比如1 1 2可以但(a b) c a (b c)不行。遇到后者还在硬用rfl编译器就会报错说明你需要rw、simp或归纳法。第二类rw方向写反。Lean 里rw [h]表示从左到右重写也就是当h : A B时把目标中的A替换成B如果你想反过来用需要写rw [← h]。方向一错目标往往越重写越乱。第三类目标本身是复合命题时没有先拆解。比如目标里出现P ∧ Q不能直接在那上面rw一般要先constructor把目标拆成两个子目标分别证明出现P ∨ Q时可能要用left或right选择一边。新手最容易在这里卡壳看到目标类型复杂就懵掉。第四类选错了归纳变量。多条变量同时出现时要谨慎选择对谁归纳。比如证明交换律时通常对第一个变量归纳会比较顺如果对第二个变量归纳往往要做额外的对称处理。选错变量后不是完全不能证但过程会明显变痛苦。5.3 和 AI 协作时的破绽识别AI 生成 Lean 代码时有一个典型问题它会把 Coq 或其他证明助手的语法混进来。比如destruct、assumption这类词在 Lean 4 里很可能不是预期中的策略。我的判断方法是看到 AI 给出一个我完全没见过的策略名先查一下 Lean 数学库文档或者干脆在 Lean 文件里用#check验证一下相关定理是否存在。#check是调试利器。比如你不确定Nat.add_comm是否正确直接写#check Nat.add_comm如果 Lean 没有报错并显示它的类型是∀ (a b : Nat), a b b a说明这个名字真实存在且类型正确。如果报unknown constant那就是 AI 编造的定理名。另一个破绽是 AI 生成代码时经常无视当前证明上下文。它不知道你的局部变量叫ih还是h₁也不知道你已经引入了哪些假设。所以最好的做法是在提示词里附上当前环境的完整报错片段或者手动告诉它“我已经有归纳假设ih : (a b) c a (b c)”。上下文越完整AI 生成的代码越接近可编译。5.4 值得刻进肌肉记忆的调试命令我平时最常用的调试三板斧#check Nat.add_assoc -- 查看定理类型 #print Nat.add_comm -- 打印定理定义 #eval (List.range 10).map (fun n n * n) -- 执行一段可计算的代码遇到“该用什么引理”的困惑时#check就是最快的检索方式。数学库 mathlib 里的定理命名大多遵循规律比如add_assoc表示加法结合律add_comm表示加法交换律mul_one表示乘以 1 等于自身。你按命名规律猜一个再#check验证基本能解决一半问题。6. 给入门者的资源与路线建议6.1 用“游戏化”方式建立直觉如果完全没接触过 Lean我特别推荐先玩一下 Natural Number Game。它把自然数和归纳法做成一系列互动小关卡要求你用类似 Lean 的策略完成证明通关后你会对rw、induction、constructor等策略形成直觉。而且它是在真实 Lean 环境里运行的玩通关的关卡本质都是在做真证明。之后可以看官方文档《Theorem Proving in Lean 4》。我不建议一上来就整本啃而是把它当工具书遇到by_cases不明白去查对应章节想知道simp能不能用翻一翻自动化策略部分。配合真实的小证明项目学起来才不枯燥。6.2 不要一口吃成胖子保持“小目标”策略很多人的心态是我要不要直接挑战一个数论里的著名定理我的建议是暂时打住。Lean 入门很容易在“大目标”上挫败。更可行的路线是每天证明一条两行的命题比如theorem my_add_zero (n : Nat) : n 0 n : by omega theorem my_double_even (n : Nat) : ∃ k, n n 2 * k : by use n omega这些命题虽然小但每次都能完整经历“理解目标、选择策略、编译器验收”的循环。等这些变成肌肉记忆再逐步尝试更复杂的定理比如质数无穷、区间上的不等式、组合恒等式等。从 AI 工具角度看LeanCopilot 这类社区插件正在快速迭代未来很可能出现更成熟的“AI 预测 proof search”。我个人的态度是工具大胆用但学习时一定要先手写再让 AI 检查。如果你连一个简单归纳法的calc版本都写不出来AI 给你做再多辅助你也只是在围观它表演而不是真正在做形式化验证。最后说一点我的真实感受。一开始我也指望 AI 直接把整条定理锤出来结果它要么给我一堆 Coq 语法要么悄悄用sorry敷衍我。后来我把心态换成了“AI 是快速查 lemma 的助手编译器才是唯一裁判”效率反而高了很多。在 Lean 里任何听起来很有道理但过不了编译器的论证都只是漂亮的废话。如果你已经把第一条rfl的波浪线等成了绿色那恭喜你你已经踏进形式化验证的大门了接下来的过程就是反复证明、反复报错、反复修改。Lean 的回报很慢但每次看到证明通过那些本来要靠“笔误修补”的数学严谨性焦虑都会被冲得很淡。