用编译器验证数学证明：Lean语言与AI结合实战教程

1. 先说人话Lean是给数学命题写“编译期检查”的那门语言第一次听说“用编译器验证数学证明”我脑子里冒出来的是那句经典质疑“编译器不就是一个会查类型的工具吗它怎么知道我证明得对不对”后来真正上手Lean语言写了几十个命题、跑通了不少证明之后我才意识到这个印象虽然不够精确但方向完全没错——Lean确实把“证明”变成了一个可以被编译器逐条检查的“类型正确的构造”。你可以把它想象成一位极其严格、不会通融的审稿人你交上去的每一步推理它都要当面验算一遍验不过就拒绝接收。这几年Lean热度持续走高其实是两条线在同时推进。一条来自数学社区大量经典定理被搬进mathlib这个形式化数学库里逐条编译验证另一条来自AI社区大模型生成的数学推理经常“看着合理、实际翻车”大家急需一个硬性的裁判Lean恰好就是这个裁判。所以现在只要聊数学定理证明几乎绕不开Lean和AI的搭配。这篇教程打算从最基础的地方讲起编译器凭什么敢验证数学证明它的内核机制是什么然后带你从装环境开始亲手写完几个能通过检查的证明最后聊聊AI在Lean工作流里到底能帮上多少忙。适合有编程基础、但第一次接触形式化验证的读者。不需要你懂很深的形式逻辑跟着敲完例子你就能理解整套机制是怎么转起来的。1.1 它和普通编程语言到底差在哪里如果你写过Java、C或者Python脑海里“编译器”这个词通常意味着语法检查、类型检查、生成可执行文件。Lean表面上也做这些事但它处理的对象不一样。在普通语言里你写一个函数声明参数类型和返回类型编译器检查函数体是否满足这个签名在Lean里你写的“类型”本身就是一条数学命题比如∀ n : Nat, ∃ m : Nat, m n而“函数体”则是这条命题的证明构造。这个区别非常关键。普通程序的目标是“让机器完成计算”编译检查是为了防止你写出类型错乱、运行时爆炸的代码。Lean的目标是“让机器验证你的推理成立”编译检查实际上就是在做数学审稿。你在Lean里写的theorem本质上是在声明一个类型而by ...后面那一堆策略命令是在指挥编译器帮你构造出一个符合这个类型的对象。用程序员熟悉的类比来说一个函数声明了“我要返回一个整数”编译器就得确认你return的位置确实是整数在Lean里命题1 1 2也是一个类型编译器得确认你后面给出的证明项属于这个类型。这就是为什么大家叫它“数学证明的编译器”因为它真的在编译期就把整条推理链路检查完了。1.2 为什么现在聊Lean总要带上AI最近几个月的热搜词里“Lean语言”和“AI”几乎捆在一起出现不是没有原因的。大模型在数学推理上有个很尴尬的现状它能用自然语言写出一段非常像样的“证明过程”但中间的某一步可能悄悄把一个符号放错了位置甚至使用了根本不成立的变换。人类读起来容易忽略这种细节因为人的阅读会自动补全逻辑漏洞而数学对漏洞零容忍。这时候Lean的价值就出来了。不管AI生成的证明片段看起来多么顺滑最终都必须喂给Lean编译器做检查。检查不过就是不过没有任何商量余地。于是AI和Lean的组合就变成了一套极其干净的“生成-检查”闭环AI负责提出候选方案Lean负责做真伪判定。你在论文里、博客里看到“先用AI生成证明再用Lean验证”说的就是这个流程。我自己的感受是目前AI写Lean还远远谈不上“全自动证明”但作为辅助工具已经很好用了。它帮你补tactic、帮你翻译命题语句、帮你从错误信息里找线索这些都很靠谱。真正决定证明能否通过的永远是Lean内核那套严格得近乎固执的检查规则。接下来我们就拆开看看这套规则到底是怎么运作的。2. 编译器凭什么敢“验证”数学证明——Lean的内核机制2.1 把命题写进类型系统要理解Lean得先接受一个看起来有点绕的设定数学命题是一种类型数学证明是这个类型的实例。这不是比喻是Lean底层逻辑的直接体现。在Lean里你可以直接检查一些表达式的类型比如在VS Code里输入#check 42 #check Nat.gcd你会看到输出分别是42 : Nat和Nat.gcd : Nat → Nat → Nat。这个好理解每个表达式都有类型。但你再试试#check (1 1 2)输出会是1 1 2 : Prop。也就是说等式1 1 2本身是一个类型这个类型属于Prop这个大类型。所谓证明1 1 2就是构造一个类型为1 1 2的项。最简单的构造方式是rfl它表示“左右两边按定义就是相等的”example : 1 1 2 : by rfl这条代码的意思就是我要构造一个类型为1 1 2的项我用rfl来充当这个项。编译器检查rfl的类型确认它确实指向1 1 2于是证明通过。这听起来可能有些抽象但程序员朋友应该能get到这不就是把“函数返回类型”的检查逻辑扩展到了整个数学命题上吗普通编译器检查一个int类型的返回值Lean检查的是一个Prop类型的证明项。底层机制惊人地一致这正是“命题即类型”这句话的真实含义。2.2 极小化可信计算基内核就是那个固执的检查员如果把Lean比作一家出版社那“内核”就是那位只认死理、绝不放水的终审编辑。整个Lean系统其实分两层外层是一大堆方便人类使用的工具比如各种策略、宏、自动化搜索工具它们负责把人类写的“半成品证明”翻译成机器能懂的原始证明项内层是一个小得多的检查器叫做kernel它只负责一件事判断一个证明项是否符合声明的类型。这个设计有一个专有名词叫“极小化可信计算基”TCB。意思是整个验证系统里我们最终必须信任的那部分代码越少越好。外层工具可以写得非常灵活、非常复杂甚至偶尔有bug都行因为再花哨的工具生成的结果最后都要交到内核手里重新检查一遍。内核的规则极少怎样判断两个类型定义相等、怎样展开定义、怎样做约归。这些规则简单到可以用少量代码实现也因此更容易被严格审查。为什么这件事对“验证数学证明”如此重要因为如果你要验证一个数学定理绝对不能依赖一个几百MB、行为复杂的编译器——那样的话证明正确与否就依赖于这个巨无霸编译器有没有bug了。Lean把最终裁判压缩成一个小小的内核所有高级工具都只是“生成候选证明”的助手。这个架构思想说得直白一点就是“外界的工具再花哨末了也得过内核这一关”。这也是Lean能用来形式化经典数学定理的重要底气。2.3 从策略到证明项人和编译器之间怎么对话新手刚接触Lean时最常见的困惑是我在by后面写的是啥为什么我写了simp、omega这种看起来像命令的词编译器就知道我在证明这就要搞清楚策略tactic的作用了。by后面的内容是策略模式下的一连串指令。你可以把它们理解为“给编译器下达的构造指令”把目标化简、把某个假设应用到目标上、做归纳假设、用线性算术搜索器穷举等等。每执行一条策略Lean都会更新当前状态——要么把目标改写得更简单要么拆出子目标要么直接构造出证明项的一部分。当所有目标都被清零证明项也就完整了。举例来说你用omega证明一个自然数不等式底层的策略执行器可能会尝试大量算术变换最终拼出一个证明项。这个证明项可能非常冗长完全不适合人阅读但没关系只要内核检查它符合命题类型就行。你可以随时用#print查看证明项的底层结构但我个人平时很少这么做因为策略生成出来的玩意儿根本不是给人读的。这个设计有一个实际好处你写证明时可以不用关心底层证明项长什么样只需要关注当前目标、当前上下文和下一步该用什么策略。VS Code里Lean插件会实时在左侧显示当前目标相当于给你开了一个“证明调试器”写证明的体验非常接近写代码时看变量值变化。3. 新手快速上手从装环境到写出第一个被编译器接受的证明3.1 安装Lean 4和VS Code5分钟把环境跑起来如果你之前被C编译器安装折腾得够呛那Lean这套反而简单。官方推荐的路径是用一个叫elan的工具来管理Lean版本它的用法和rustup几乎一样。打开终端执行curl -sSL https://get.lean-lang.org/elan-init.sh | sh脚本跑完后elan会安装到本地。接着安装Lean 4稳定版工具链elan toolchain install leanprover/lean4:stable这一步会把Lean编译器、标准库和配套工具都装好。然后是创建工程。Lean的自带构建工具叫lake类似Cargo或npm。新建一个项目lake new lean_demo cd lean_demolake new会生成一个目录里面有Lean文件夹和一个lakefile.lean。默认工程模板里有一个Main.lean文件你可以直接在里面对应的地方写证明代码也可以新建一个.lean文件。接着用VS Code打开这个目录在扩展市场装一个叫“Lean4”的官方插件装好后打开任意.lean文件插件会自动加载Lean环境。注意如果你之前刚折腾完VSCode的C编译器可能会习惯性地到处找“编译器路径”之类的配置。Lean这边不用。插件是通过elan自动找到Lean可执行文件的你只需要保证项目根目录有lakefile即可。最后跑一下工程lake build如果一切正常说明环境没问题。第一次进入工程时如果你的项目依赖了mathlib这个大数学库构建过程会比较漫长可能要等一段时间下载和编译。我建议新手先不加mathlib依赖后面需要某些数学定理时再加上否则首秀会被编译时间劝退。3.2 常用声明和第一份“编译通过的证明”先把最常用的几个命令搞清楚它们是新手“喂给编译器”的日常工具命令作用示例#check查看表达式的类型或定理的完整类型签名#check Nat.add_assoc#eval执行一个可计算表达式输出结果#eval 1 1example声明一个待证明的命题只做临时验证example : 1 1 2 : by rfltheorem声明一个正式的定理后续可以复用theorem my_add_assoc : ...lemma和theorem类似通常用于辅助引理lemma add_zero : ...写进一个.lean文件里试试import Mathlib -- 如果你用了标准模板通常会带 #check Nat.add_assoc #eval 1 1 example : 1 1 2 : by rfl左边VS Code的Lean面板会展示#check的结果Nat.add_assoc : ∀ (a b c : Nat), a b c a (b c)。这个类型签名本身就是一个命题也就是说Nat.add_assoc这个定理已经是“一个类型为加法结合律命题的项”我们后续可以把它当作证明构件拿来用。这就像你在普通语言里调用一个函数它已经存在你只需要告知编译器“我想用它”。刚上手时我的建议是先养成“先声明、后证明”的习惯。先用example或theorem把命题写清楚再在by后面逐步用策略完成任务。看到左边目标窗口变成“No goals”编译器才会给好脸色。3.3 手动完成一个带量的数学证明光是一个1 1 2不过瘾我们来点更带感的。先试一个最常见的自然数命题对任意自然数n都有n 0 n。注意这个命题在自然数定义里并不完全平凡因为加法的定义是递归地展开第一个参数。在Lean里可以这样证明lemma add_zero_right (n : Nat) : n 0 n : by induction n with | zero simp | succ n ih simp [ih]我来逐行解释编译器在这个过程中到底检查了什么。第一行induction n with把证明变成了两个子目标基例0 0 0和归纳步Nat.succ n 0 Nat.succ n。基例里simp可以根据自然数加法的定义直接把左边化简成0于是目标变成0 0编译器接受。归纳步里ih就是我们归纳假设n 0 n而目标左边Nat.succ n 0会在加法定义下展开成Nat.succ (n 0)simp [ih]用归纳假设替换掉n 0得到Nat.succ n Nat.succ n完成。这个例子不大但在入门教程里很经典因为它第一次让你“看见”编译器在检查归纳证明里的每一步归纳假设被明确声明出来替换时编译器要核对类型完全一致。你写错任何一个地方左侧目标窗口就会立刻变红告诉你哪一步没对上。example (a b c : Nat) : (a b) c a (b c) : by exact Nat.add_assoc a b c更复杂的命题比如加法结合律直接用标准库里现成的定理Nat.add_assoc就能一行解决。exact的作用是“我要把一个已知的项作为完整证明递给编译器”编译器检查它的类型和当前目标是否完全一致。如果类型不一致它会直接报type mismatch。这三个小例子跑通了你就完成了从“写代码”到“构造证明项”的初次体验。4. AI在Lean工作流里到底能干多少活4.1 AI补全tacticCopilot这类工具的真实体验把AI拉进Lean工作流最朴素也最实用的场景就是让AI补全by后面的策略。我在VS Code里用GitHub Copilot写Lean代码时它经常能猜到我想用的定理名。比如我写了example (a b c : Nat) : a (b c) (a b) c : by停在换行处Copilot会建议exact Nat.add_assoc a b c。这个建议恰好能用因为加法结合律定理的方向、变量顺序它都对了。但AI的建议不能盲信。有一次我想证明一个关于乘法的简单命题它给我建议了rw [Nat.mul_comm]我一看就知道这是把交换律当成化简规则在用确实没问题可另一次它给我推荐了一个从没见过的定理名我猜大概是它“捏造”出来的跑一下#check编译器立刻报unknown identifier。这让我彻底明白AI生成的文本只是候选方案MVP最小可行证明不是它说了算是编译器说了算。值得提一下的是Lean插件本身也内置了一些基于搜索的策略建议比如当你把光标停在某个目标上时插件会提示有哪些常量和simp定理可以用于当前目标。这类建议比大模型凭空生成的更可靠因为它的候选集来自已经导入的库。我的习惯是先用插件自带建议探路再用AI补全作为加速工具最后永远以编译器的检查结果为准。4.2 让AI帮我把自然语言命题翻译成Lean声明“把自然语言数学命题翻译成Lean代码”是我觉得AI目前最有价值的用法。数学证明的难点常常不在纯推理而在于你要先写对命题的正式表述。比如你有一个自然语言命题“如果两个自然数相等那么它们的平方也相等”让AI翻译成Lean代码它会给你theorem sq_eq_of_eq {a b : Nat} (h : a b) : a ^ 2 b ^ 2 : by rw [h]这个声明其实已经猜到了关键h : a b是前提假设rw [h]在目标里把b替换成a目标变成a ^ 2 a ^ 2于是证明完成。这个例子说明AI对Lean语法和常用策略已经有不错的“语感”。但坑也很多。AI有时会把命题里的省略信息脑补错比如把“存在一个大于所有自然数的自然数”翻译成看似合理但是假命题的表达式更常见的是漏掉量化符的括号范围。我的应对办法是三步走第一步让AI把命题翻译成theorem声明第二步立刻用#check检查这个声明的类型是否合理第三步如果后面要手写证明再回到VS Code里对着目标逐步推进。不管AI翻译得多么像样只要#check报错或者编译失败就得回头改这一点没有任何回旋余地。4.3 为什么AI写出来的证明必须过Lean这一关AI写数学证明本身就有点“黑盒表演”的味道。大模型没有内置逻辑真值的概念它只是根据上下文生成一串看起来合理的符号。在数学这种一步错、步步错的场景里这种“看起来合理”是最危险的。Lean给这个危险世界装上了一道硬性闸门内核检查不过证明就不成立。这个机制的价值怎么强调都不过分。也正是因为这一点现在很多数学和AI交叉的研究会把Lean当作“测试场”让模型在Lean环境里做证明每生成一步编译器就实时反馈对不对。模型通过试错、编译错误信息、目标状态来调整策略最终完成证明。这个模式下的“证明成功”是真实可信的因为它过了内核检查而不只是模型自己觉得“应该对了”。当然也别神化这个流程。Lean验证的是“在给定公理和定义下命题成立”至于这些公理是否刻画了现实世界那是另一个问题。但至少在我们关心的数学推理内部AI加Lean的组合能真正把“生成”和“验证”拆开生成可以用模糊的启发式验证必须用严格的形式化。我个人非常看好这个方向因为它终于让AI在数学领域学棋手和棋谱的关系模型负责出招验证器负责结论。5. 常见报错和排坑实录5.1 高频报错unknown identifier、type mismatch新手在Lean里遇到最多的三种错误我把它们整理成了一张速查表按实际踩坑频率从高到低排列报错信息大概率原因解决办法unknown identifier xxx定理名打错了或者没有import对应的库用#check确认名称确认import Mathlibtype mismatch你提供的证明项类型和目标不一致用#check查看目标类型检查参数顺序和变量绑定关系unsolved goals策略执行完还有子目标没被处理查看左侧目标窗口继续用策略解决剩余目标举一个真实的例子假设我想证明加法交换律的一个特例却在策略里写example (a b : Nat) : a b b a : by exact Nat.add_assoc a b a这行代码会直接报type mismatch因为Nat.add_assoc给出的类型是a b c a (b c)和当前目标a b b a的左右两侧方向、结构完全不同。编译器不会因为我们看着“这俩都有加法”就通融。遇到这种报错我的排查顺序是先看目标窗口里当前目标长什么样再看我提供的项类型是什么最后用change或者更合适的策略比如omega、rw [Nat.add_comm]修正方向。5.2 内存不足、heartbeat超时这类工程问题如果你的证明比较复杂或者策略跑得太深Lean会报类似maxHeartbeats exceeded的错误。所谓heartbeat是Lean给策略执行设定的计算预算防止一个自动策略无限搜索下去。遇到这种情况可以在证明前面加一句set_option maxHeartbeats 4000000把预算调大让自动化策略有更多时间搜索。如果预算调到极大还是跑不完那大概率不是预算问题而是策略本身不合适需要换一条更聪明的路径。另一个常见问题是编译大型库时内存吃紧也就是大家常说的“编译器堆空间不足”。我第一次编译mathlib的时候内存小跑一会儿就爆了后来发现是可以控制的。用lake build -j1限制并行度让编译任务一个一个来能显著降低峰值内存。如果电脑内存实在不够建议先在较小的库上练习不必一上来就编译完整版mathlib省心很多。5.3 从C/Java带过来的“main类型”困惑在热搜词里有一句“编译器未包含main类型”这个报错常见于C或Java新人配置编译环境时。很多第一次接触Lean的人顺手把这个困惑也带进来了我是不是必须在工程里写一个main函数编译器才肯干活答案要分场景。用lake new lean_demo创建的默认工程通常包含Main.lean里面会有def main : IO Unit : ...这样一个入口如果你把它改成纯数学证明工程那就不需要main了。事实上你在一个.lean文件里写的example、theorem、lemma本身就会在编译时被检查不需要任何程序入口。main只和“可执行程序”有关和“数学证明库”无关。把这两件事分开就能避免把其他主流语言的习惯误带到Lean里。我的经验是写数学证明时几乎可以不去碰main。你只需要把注意力放在theorem声明和左侧的目标窗口上编译器会像对待一个库工程一样逐个检查你的证明是否成立检查完了就通过不要求你提供一个可运行的程序的入口。6. 一点个人体会写这篇教程的过程其实也是我重新反思“证明”的过程。以前我看到一段数学证明脑海里会自动省略一些“显然”的步骤而Lean最不买账的就是“显然”。它逼着我把每一步推理都变成编译器能查的对象这个体验一开始有些难受用久之后反而上瘾。最后分享几个我一直在用的土办法。第一遇到一个目标先用simp和omega探路能自动解就自动解解不了再手写归纳第二写证明之前永远先确认theorem声明本身没有歧义声明错了后面全是白干第三AI生成代码尽量当草稿用让它负责提速让Lean负责把关两者各司其职是最舒服的配合方式。希望这篇教程能让你少走一些弯路早日享受“编译器给你过证明”的踏实感。