我第一次听到“Lean编译器验证数学证明”这句话时脑子里冒出来的疑惑是编译器不是用来把C变成机器码的吗怎么还能验证数学证明这个疑惑一直持续到我真正在电脑上装好Lean、敲下第一段证明代码看到编译器在几毫秒内给出“证明正确”的反馈那一刻才彻底反应过来——原来数学证明本身就是一种可以交给机器检查的“程序”。这篇内容不是什么学术论文的压缩包而是一份面向零基础入门者的详细操作笔记。我会尽量用“程序员写代码”的思路来解释“数学家写证明”这件事把Lean到底是什么、为什么它能验证证明、怎么装环境、怎么写第一个定理以及AI大语言模型和Lean之间目前能怎么配合一件一件说清楚。如果你以前没有接触过函数式编程、没有系统学过数理逻辑也不影响阅读我会在关键位置把基础概念补上。1. 编译器如何成为数学证明的“裁判”1.1 数学证明也可以被“编译”传统意义上的编译器做的是“高级语言 → 机器码”的翻译并且在这个过程中检查语法、类型、变量作用域等各类错误。而Lean做的事情在逻辑结构上惊人地相似它把你写下的每一个数学命题当作一个“类型”把你提供的每一个证明当作这个类型的一个“值”或“实例”然后它只做一件事——检查这个“值”的类型是否真的匹配那个“命题类型”。如果你没有接触过类型论这句话可能会有点绕。我换个生活化的说法你可以把命题1 1 2想象成一把锁把“证明112的证据”想象成一把钥匙。Lean这门语言内置了一个极其严格的“锁匠协会”它不管你的钥匙是不是金的、是不是好看它只关心一件事这把钥匙能不能插进锁芯能不能转动。如果转得开它就通过如果转不开它就报错。整个过程完全机械化不需要评委投票不需要参考“这个证明风格好不好”只看“逻辑构造是否严格有效”。这个思路最早可以追溯到Curry–Howard对应也就是“证明即程序、命题即类型”的核心理念。简单说一个数学命题被编码成一个类型一个合法的证明就是该类型的一个项只要程序能通过类型检查就等价于证明在逻辑上成立。Lean就是把这一套理论工程化、产品化的最佳实例之一。1.2 为什么选Lean而不是其他证明助手市面上做形式化验证的证明助手其实不少Coq、Isabelle、Agda、Rocq都有各自的拥趸。我在入门之前对比了一段时间发现Lean有非常明显的几个现实优势社区活跃度高。Lean自2013年发布以来迭代到Lean 4目前维护积极数学库Mathlib已经包含大量现代数学定理社区可以说相当活跃遇到问题去GitHub和Zulip聊天室提问基本能很快得到回应。依赖类型和可编程性极强。Lean本身是一门完整的高级编程语言不像某些证明助手那样把“证明逻辑”和“程序语言”割裂成两套体系。你可以在Lean里同时写可运行的算法和数学证明。语法相对友好。虽然它仍然是个函数式语言但相比Coq的Gallina语法Lean的语法更接近程序员的直觉很多tactic证明策略的名字也比较好猜比如simp化简、omega解线性算术、ring算环等式。自动化能力突出。Lean 4自带的tactic库加上Mathlib中大量的自动化工具让“写证明”这件事越来越接近“给编译器描述思路编译器帮你抠细节”。当然Coq在工业界和某些特定方向也有不可替代的地位Isabelle在交互式证明上也久经考验。但如果你是为了“学习用计算机验证数学证明”并且希望尽快跑通流程、保持学习动力Lean是当前综合体验最好的选择。2. 搭建Lean开发环境别在第一步就放弃很多入门者会被第一个门槛劝退——不知道怎么安装、不知道装哪个版本、不知道“那个编辑器插件提示到底有什么用”。根据我自己的实测经验这里给你一套完整的、能走的通的操作路径。2.1 安装Lean 4与编辑器扩展如果你用的是VS Code过程会非常顺滑。安装VS Code在扩展市场搜索Lean4安装微软官方出品的“Lean 4”扩展安装Lean工具链。最省心的方式是通过官方脚本elan它是Lean的版本管理器类似Rust的rustup。打开终端执行curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh安装完成后使用elan default stable将其设为默认版本。然后重新加载VS Code窗口扩展会在你打开.lean文件时自动下载配套的Lean服务端。如果你不想依赖网络下载也可以直接用elan安装指定版本elan toolchain install leanprover-4.14.0这个步骤的本质是让编辑器拥有一个“语言服务器”和你写C时使用clangd或intellisense非常类似。Lean扩展会在你输入时实时把当前证明状态、错误信息推送到侧边栏这个实时反馈就是以后你写证明的主要“仪表盘”。2.2 创建项目并加载Mathlib单独装好Lean其实只能做最基础的练习真正有实用价值的证明大多依赖于Mathlib数学库。建议用Lean自带的包管理器Lake来创建项目lake new hello_math cd hello_math lake update mathlib然后你需要在lakefile.lean里确认已经添加了require mathlib from git ...这一行并执行lake exe cache get这一步会下载Mathlib的预编译缓存体积比较大可能得花上几分钟甚至更久。千万不要跳过否则你在写import Mathlib的时候会被漫长的编译过程折磨到怀疑人生。接着在Hello.lean里写入import Mathlib #check Nat.add_comm把光标放在#check Nat.add_comm那一行Lean 4扩展的Infoview里会显示这条定理的类型。如果显示正常说明环境和Mathlib已经跑通了。2.3 新手最容易遇到的环境问题第一个问题是版本混乱。目前网上很多老教程是Lean 3的内容而你现在应该装Lean 4。Lean 3的语法和tactic体系和Lean 4差距很大照着旧教程写大概率会报错。判断方法很简单看文件第一行有没有import Mathlib以及代码里用的是theorem还是lemma这些在新旧版本中都有差异。第二个问题是你可能已经装了Lean 3的VS Code扩展它与Lean 4扩展同名但不同包。请在扩展列表里先禁用或卸载带有“Lean 3”字样的旧扩展只保留一个。第三个问题在国内网络环境下下载Mathlib和elan脚本可能会比较慢。这不是什么教程能绕过的只能耐心等待或者换一个网络条件好的时间段反复重试。多试几次一般能成功。3. 看懂Lean证明核心语法与思维转变环境装好之后真正的学习才刚刚开始。这个阶段最难的不是记住某个函数名而是完成一次“思维转变”——从一个“我要怎么算”变成“我要怎么证明”。3.1 命题就是类型证明就是程序在Lean的世界里Prop是一种特殊的类型用来表示数学命题。一个命题P : Prop本身是一个类型P的“元素”就是该命题的证明。如果你能构造出一个类型为P的项就相当于给出了P的证明。举个例子example : 2 1 1 : by rfl这个example声明了一个命题2 1 1。冒号后面的部分是命题by后面是证明脚本。rfl表示“由定义计算可知两边相同”它会告诉编译器“把2逐步化简为11发现两个表达式本来就相同”。编译器检查后如果类型匹配就通过。这个例子看起来像废话但它揭示了一个核心思想Lean不靠直觉判断对错它靠的是“证明项”的类型能否匹配“命题”的类型。你在by块里写的每一个tactic最后都会变成一个具体的证明项而这个证明项就是程序是可以被内核检查的。3.2 常用tactic速查表刚开始写证明不需要掌握太多tactic下面这几个够你走完第一个实战项目Tactic作用直觉类比intro x把∀ x对于所有x变成引入一个具体变量相当于“任取一个x我们来证明……”对应数学证明里“设x为任意给定……”rfl利用定义上的相等性直接证明等式相当于“按定义展开两边一模一样”rw [h]把目标里的某一处用已知等式h重写相当于“利用已知结论h把表达式替换成等价的另一形式”simp调用化简器自动使用许多定义和引理来化简目标相当于“傻瓜化简”但有时会自作聪明exact h当前目标已经被某一项h完全解决相当于“这个我已经证明过了/现成的证据在这里”apply h用h : A → B来把目标B转化为A相当于“为了证明B根据已知的h我只需证明A”omega解决自然数或整数上的线性算术命题相当于“这一步所有线性不等式/等式机器直接算”ring解决交换环上的多项式等式相当于“展开括号、合并同类项机器最擅长”linarith解决实数和线性算术的不等式等价于解联立线性不等式这些tactic的命名其实都很好记simp是simplifyrw是rewriteintro是introductionexact就是“恰好命中”。3.3 从“命令式编程思维”切换到“证明状态思维”我见过太多程序员上手Lean时最大的障碍就是脑子里总想着“我先算什么再算什么”。Lean里的证明过程更像是“当前目标只有一个我选用哪个策略来逐步把它化解成若干个更小的子目标最终全部解决”。每次tactic执行之后编辑器侧边栏的Infoview会显示目标 (Goals) ⊢ n 0 n这个⊢符号右边的就是当前待证明的命题冒号左边是上下文也就是你已经知道的条件。你可以把整个写证明的过程想象成玩拆积木你不断调用tactic把一个大目标拆成小目标直到每个小目标都被rfl、exact、simp这类“终结技”干掉。这种思维转变需要一点时间但它一旦转过来你看数学证明的角度会彻底变化——证明不再是“一段雄辩的文字”而是“一步步被拆解、被机器确认的构造过程”。4. 完整实战从加法结合律到平方差公式理论说得再漂亮不如亲手跑通一个例子。这一个小节我会带你从最简单的自然数定理开始一步步写出能够在Lean编译器里通过的证明。建议你跟着开一个Test.lean文件实际操作。4.1 第一个定理自然数加法的结合律自然数加法结合律是(a b) c a (b c)这个定理在教科书里通常作为皮亚诺算术系统的公理或基础定理。在Lean中Mathlib已经给出了通用证明但我们自己一步步来。import Mathlib theorem my_add_assoc (a b c : Nat) : (a b) c a (b c) : by induction a with | zero simp | succ a ih simp [ih]解释一下发生了什么induction a with表示对a做数学归纳法。zero分支处理a 0的情况左边变成(0 b) c右边变成0 (b c)根据加法的定义两边都化简为b csimp直接通过。succ a ih分支处理a a1的情况此时归纳假设ih告诉我们(a b) c a (b c)已经成立。simp [ih]会把(succ a b) c按定义展开成succ ((a b) c)再把succ (a (b c))和右边对齐最终利用归纳假设ih完成。如果你把光标停在by后面、induction a with执行完的位置你能看到两个待证目标这正是“当前目标”这个概念最好的体现。这就是数学归纳法在类型论中的执行方式编译器要求你分别处理zero和succ两个分支并且允许后者使用归纳假设。4.2 实战平方差公式选择合适的数据类型平方差公式(a b) * (a - b) a^2 - b^2在自然数范围内会遇到一个非常经典的坑自然数的减法被“截断”了3 - 5 0。所以如果直接用Nat这个公式其实并不总是成立比如取a2, b5。正确的做法是先在整数Int范围内证明theorem sq_diff (a b : Int) : (a b) * (a - b) a^2 - b^2 : by ringring这个tactic可以直接展开所有多项式运算几毫秒就结束。你可能会觉得“这也太作弊了”但不要小看这个过程——ring并不是魔术它内部实现了一套完整的环论求解算法并且每一步推导都会被Lean内核重新验证。你不需要手写十几个分配律重写你的工作是“选择正确的代数结构、识别适用的自动化工具”。如果把题目改成在自然数上做theorem sq_diff_nat (a b : Nat) (h : b ≤ a) : (a b) * (a - b) a^2 - b^2 : by have h : (a - b : Int) (a : Int) - b : by omega -- 思路把整个等式转入Int利用整数上的结果这里引入条件h : b ≤ a是为了保证a - b在自然数中不会被截断。这个小小的改动体现了数学家和形式化验证者之间一个重要的默契同一个公式在不同代数结构里可能有完全不同的成立条件形式化能逼你把每个隐藏假设都显式写出来。这种“显式化”能力正是Lean训练数学思维的核心价值。4.3 编译器到底是怎么检查证明的你每次执行by ...块Lean里的elab过程都会把tactic脚本展开为一个完整的证明项也就是一个依赖类型的 λ 项。这个项由Lean的信任内核kernel做最后的类型检查。如果你写了ringtactic会构造出一个庞大的证明项其中包含了所有运算规则的调用链内核去检查这个项的类型是否为a^2 - b^2 (a - b) * (a b)的某个等价形式。这个设计的巧妙之处在于tactic本身可能会出错自动化工具可能写得有bug但内核只做非常小、非常基本、非常慢的类型检查规则。只要内核实现正确最终证明就不会出错。这就好比考场里你可以用计算器做快速运算但“判断题一个证明是不是有效”这件事监考老师始终坚持最原始、最不可简化的步骤来检查。这也是为什么Lean敢于宣称“由内核验证过的证明是正确的”——整个体系的安全性被收敛到了一个小而精的检查器上而不是一个庞大复杂的自动化工具链上。5. AI时代的Lean大模型如何辅助写证明5.1 Lean自带的自动化工具算式里的“AI代理”“AI辅助写证明”这个话题很多时候被想得太玄。其实Lean生态里早就有一批tactic可以承担“自动找证明”的重任它们本质上就是运行在本地的专用自动化引擎。simp负责化简表达式自动匹配数百条化简引理aesop是一个基于规则搜索的自动化证明策略适合构造性逻辑的证明omega和linarith专门解决线性算术问题ring和ring_nf专门处理环论中的多项式等式assumption会自动检查当前上下文里是否已有目标所需的条件。我在写证明时常常使用的做法是先simp不行就omega再不行就ring这些tactic就像是三个不同专业的“小助手”。传统数学家用草稿纸演算我们今天的做法是把这些“小助手”当成AI代理来差遣。5.2 大语言模型补全Lean证明草稿的正确姿势ChatGPT、Claude这类大语言模型在处理Lean代码时确实能写出一些看似合理的证明片段但它们完全可能“一本正经地胡说八道”生成一个语法正确但逻辑路径不通的证明。根据我的实测经验大模型和Lean之间的关系不是“大模型替代你写证明”而是“大模型帮你生成初稿Lean编译器当最终裁判”。一个比较靠谱的工作流是这样的首先用自然语言向大模型描述你要证明的命题例如“在Lean 4中帮我写一个定理证明整数的平方差公式”。让模型生成代码框架import Mathlib theorem int_sq_sub (a b : Int) : (a b) * (a - b) a * a - b * b : by ring然后把这段代码粘贴进Lean文件让编译器做检查。如果报错把报错信息原样复制给大模型让它修改。这个过程的本质是把大模型当作一个“能理解自然语言和代码的tactic生成器”而真正把握证明有效性的、最终拍板的永远是Lean编译器。我见过很多初学者拿着大模型生成的“看起来很对”的证明直接发到网上结果一编译全是错。正确的心态应该是AI生成的东西是草稿编译器是权威。所有AI输出的证明都必须经过内核检查才算数。5.3 人类的价值拆解命题、选择策略目前大模型在Lean上的弱点是缺乏深度的证明结构理解。它们擅长单一策略的证明但在多步骤、需要构造复杂中间引理的证明上往往会卡住。这时候真正有价值的人类工作是把一个大定理拆解成若干个小引理判断该用什么代数结构、什么归纳方式分析为什么当前的策略失效换一个证明思路给大模型提供中间条件的提示让它生成对应的引理证明。简单说现在AI辅助写证明的格局是“人负责战略AI负责战术”。工具越强你需要掌握的核心数学思维越重要。因为如果你自己都不清楚为什么a - b要在Int上写、为什么需要条件b ≤ a那无论多好的AI助手都会把你带到沟里去。6. 入门三个月后我踩过的坑和一点心得6.1 符号输入是新手第一道坎Lean里的∀不是从键盘上直接敲出来的。在VS Code的Lean 4扩展环境里你输入\forall然后按Tab或空格它就会变成∀。同样→输入\to∈输入\in≤输入\le≥输入\ge。你还可以用\a、\b输入花体字母\aleph输入阿列夫。这一点和LaTeX非常像。还有一个技巧把鼠标悬浮在Infoview里的数学符号上VS Code会显示对应的输入序列。这个功能对新手来说非常救命我第一次知道可以这样查符号时写代码效率翻了一倍。6.2 别让simp替你包办一切simp好用是真的好用但它的副作用是“它把你该思考的东西也藏掉了”。你不明白它为什么能通过一旦换一个类似的命题它不化简了你就彻底抓瞎。我推荐的做法是初学者阶段每一次simp都能成功通过后试着把它换成rw或exact系列手动把化简过程中的关键引理找出来。比如看这一条example (n : Nat) : n 0 n : by simp换成不用simp的版本example (n : Nat) : n 0 n : by rw [Nat.add_zero]看到rw [Nat.add_zero]之后你才会真正知道“哦原来这是加法定义里的零元规则”而不仅仅是“反正simp搞定了”。这是从“会操作”到“真理解”的关键一步。6.3 证明卡住时检查你的“假设边界”这是我在Lean上花时间最多的地方。很多次证明写不下去并不是tactic不行而是命题本身就不成立只是我在心里默认了一些条件没有写出来。比如在自然数上写a - b b a它不成立除非加上b ≤ a。Lean的报错不会替你指出“你少了这个条件”它只会告诉你“当前目标无法从上下文中推导出来”。因此一旦卡住第一件事不是急着加have中间结论而是回到数学层面问自己这个命题在什么条件下为真我是不是做了某个未声明的假设这一步排查思路对做数学同样重要——如果你正在证明的陈述本来就是假的再多的计算也救不回来。6.4 保持迭代的心态Lean的证明过程很像和一位严格的老师过招你写一行它告诉你不行你换个思路它再告诉你不行直到某个时刻它终于说“No goals”那个瞬间的成就感是其他编程语言很难给你的。初学阶段不要追求一次性通过我自己的第一个完整证明用了整整半天中间报了几十次错但只要每一次报错都至少让你对“当前目标”多了一分理解这个时间就花得值。如果你正准备入坑Lean我的建议是先把环境装好把这篇里的例子从头到尾敲一遍然后去Mathlib里找一个你熟悉的小定理比如mul_comm乘法交换律用Lean重新证明一遍。做完这一步你已经不是“听说过Lean”的人了而是“真正用编译器验证过数学证明”的人了。后面要做的就是把这种“把数学当作程序来写”的思维方式带到更多更复杂的定理中去。