从造桥到证题：Lean 定理证明器入门与核心概念

可视化演示

交互展示AI驱动形式化验证的核心流程：自然语言规约自动生成、符号执行验证管道与反例搜索策略，可视化从需求到证明的自动化闭环。

初识 Lean——给证明工地请一位数字监理

造大桥最怕什么？不是设计不出来，而是「每个环节都以为别人验过了」。一座悬索桥需要成百上千人协同，任何一环的疏忽都可能酿成事故。数学也一样，一篇论文里的证明可能长达数百页，靠人工评审有时隔很多年才能发现漏洞——四色定理、开普勒猜想这类硬仗都曾让数学家心有余悸。所以数学界一直想找一位不知疲倦、绝不客气的「监理」。

Lean 就是这位数字监理。它是一个交互式定理证明器：你输入一个命题 P，再输入一个证明 p，Lean 的类型检查器会逐字逐句核验 p 是不是 P 的合法证明，就像监理用仪器对每一根钢梁做无损探伤。这一核验是机械的、确定的：过就是过，不过就是不过。市面上还有 Coq、Isabelle/HOL 等定理证明器，但 Lean 的设计哲学非常突出：一个尽可能小的逻辑内核，加一个尽量好用的外部接口。小内核意味着可以被彻底审计，外部接口让 def、theorem、tactic 这些语法糖都只是「翻译」到内核。社区围绕 Lean 建起了 Mathlib——一个覆盖现代数学的统一知识库，规模大得常被形容为「数学的 GitHub」。

Lean 的核心推理规则之一，是逻辑学里最古老的「充分条件假言推理」：只要 A 成立，并且 A 能推出 B，那么 B 就一定成立。这在施工中就像「验收规范」：

学 Lean 的第一课，就是接受一个角色转变：你不再是凭灵感写论文的独行侠，而是带着图纸、随时接受监理抽检的施工队长。Lean 把这种「如临大敌」变成日常，但正因如此，每一座桥都真的站得住。

类型论基础——给每一块材料贴上规格标签

仓库里的钢梁不是一堆铁疙瘩，每根都有铭牌：材质 Q345、长度 12 米、屈服强度 345MPa。没有铭牌的材料不允许上桥。在 Lean 的世界里，每一块「材料」——也就是每一个表达式——也有一张铭牌，叫「类型」。类型决定了这个表达式能用在什么地方，就像钢梁的规格决定了它能架在哪一跨。

这种「值-类型」配对听起来很像编程语言里的变量类型，但 Lean 的类型远比 int、string 强大。当类型可以依赖一个变量的值——比如「对任意自然数 x，x+0=x」这个命题里，命题本身的对象随 x 变化——它就升级成了依值类型。这里藏着一把钥匙：命题即类型（Curry-Howard 对应）。命题是一种类型，命题的证明是这种类型的一个值。于是「证明一个命题」等价于「构造一个特定类型的程序」，就像「把这块钢梁加工成图纸要求的形状」等价于「按规格书一步步施工」。

Lean 的类型本身也有类型：Type : Type 1，而 Type 1 : Type 2……无穷无尽。这不是故弄玄虚，而是为了避免「所有类型都归到自身」导致悖论，就像建筑规范规定「规格书的规格书」也要单独归档——每一层都在上一层登记。宇宙层级是依值类型论的地基，也是新手最容易忽略却最关键的概念之一。

有了铭牌，监理才能验收。Lean 里输入的每一个「值」，都必须先有「类型」这张铭牌，一切后续工作都由这张铭牌展开——这就是它跟传统数学「一个命题孤零零地写在那里」最大的不同。

定义与定理——把设计图签进合同

工程师造桥前，先把「主跨 1200 米」「桥面宽 32 米」写进合同。合同不是愿望，是约束。Lean 里 def 和 theorem 就是签合同的笔：def 定义「材料是什么」，theorem 承诺「必然如此」，而 := 后面跟着的是证明，相当于施工记录。

在 Lean 中，def double (n : ℕ) : ℕ := n + n 定义了「翻倍」这个操作，相当于在仓库里登记一种新材料：名称 double，参数 n，返回值类型 ℕ，实现体 n+n。而 theorem add_zero (n : ℕ) : n + 0 = n 声明了一条桥梁设计承诺：对任意自然数 n，n 加 0 等于 n。注意，声明定理只是「签合同」，合同能不能兑现，还要看后面给出的证明是否通过监理——Lean 的类型检查器——的验收。

Lean 有「环境」概念：只有已经登记进环境的定义和定理才能被后续代码引用，正如监理验收过的桥段才允许通车。#check 命令可以随时查看某个名字的类型，像查档案；example 则用来临时验证一个小命题，不必签「长期合同」。这种「先登记、后引用」的机制保证了整个知识库的每一块砖都来自已验证的来源。

签了合同，监理才会来查。Lean 中定义与定理的边界非常清晰：定义回答「这是什么」，定理回答「必然如何」，证明负责兑现承诺——三者缺一不可，就像设计图、合同和验收报告一起构成一座桥的完整档案。

直接书写证明——一块一块钉桥板

造桥最朴素的方式，是背起桥板从这岸走到那岸，一块块钉死。直接写「证明项」就是这样原始而可靠。在很长一段时间里，数学家使用 Lean 就是这种模式：写出一个表达式，它的类型恰好就是待证命题，表达式的构造过程就是证明过程。

在 Lean 中，一个 P → Q 的证明就是一个函数：给它一个 P 的证明，它返回一个 Q 的证明。比如证明 P → Q → P，只需要写 fun hp => fun hq => hp——收下 hp 和 hq 后就地返回 hp。这段「代码」本身就是证明，因为命题即类型：命题 P→Q→P 是一个类型，而 fun hp => fun hq => hp 是这个类型的构造对象，一个合格的「项」。

这里的 fun（lambda 抽象）对应逻辑里的「蕴含引入」：把前提当成函数参数收进来。函数应用则对应「蕴含消去」。Lean 还提供 apply 做反向应用：目标是 Q，找到一条定理 P→Q，apply 之后目标就变成 P，相当于施工队先看看「要铺到 Q，有没有 P→Q 这条路」。直接写项与使用战术最终都会生成同一个构造对象，就像无论用吊车还是人工，铺上的板都是同一块预制板，只是施工方式不同。

直接写证明确实「手酸」，但它是理解一切的基础——所有花哨的战术，最终都只是帮你拼装这一块块桥板。哪怕你以后只用 tactic 写证明，心里也要清楚：tactic 生成的正是这样的 lambda 项。

战术模式——给施工队配全套机械

造大桥光靠人拉肩扛不行，得有起重机、混凝土泵车。Lean 的 tactic 战术模式，就是施工队的机械设备清单。数学家写证明，不再需要像上一节那样从零拼装 lambda 项，而是像指挥施工队一样，一步步下达操作指令。

by 打开战术模式后，Lean 会展示一个「目标看板」：⊢ 左边是当前收集到的前提，右边是还没铺通的桥段。你在看板上看到 P, Q ⊢ P，就知道前提里已经有 P，直接 exact hP 就能收工；看到 ⊢ a + 0 = a，一次 rw [add_zero] 把 a+0 换成 a，目标变成 ⊢ a = a，再 rfl 就直接通车。intro 负责把箭头前的条件收进前提库（跟 lambda 收参数是一回事）；apply 反向调用定理；rw 做等价替换；rfl 自动处理自反相等。

由于目标是逐步拆小的，「目标状态」就成了一个实时施工看板。你可以反复试验不同 tactic，Lean 立刻反馈成功或失败，就像工头在看板上看到进度条有没有前进。这种交互感让 Lean 在定理证明器里显得格外「现代」，也让 AI 模型可以在这里不断试错并获得反馈——这一点我们到最后一节还会讲到。

tactic 不是魔法，它们每一个都对应一条确定的逻辑规则，只是把「拼桥板」包装成了顺手好用的机械。所以新手不必被一堆 tactic 名字吓到——核心只需要先掌握 intro、exact、apply、rw、rfl 这五件套，就已经能读能写大多数入门证明了。

归纳类型——用预制件批量生产桥板

手工浇筑每一块桥板太慢了。现代造桥用预制构件：一个模具，批量生产，运到现场拼装。归纳类型就是 Lean 的「模具生产线」。数学里最常见的无穷对象——自然数——就是靠这条生产线定义出来的。

在 Lean 中，inductive Nat | zero | succ (n : Nat) 定义自然数：zero 是一块起始板，succ 是把一块板变成下一块板的生产线。这个小小的定义会自动生成自然数归纳原理，也就是数学归纳法：先验收第 0 块板，再证明「第 n 块合格 ⇒ 第 n+1 块合格」，就能保证整座桥无穷无尽地铺下去。归纳类型不只能定义自然数，还能定义列表、树、语法树、带索引的命题——它们共同的特点是：所有值都必须由构造子有限生成，这给了证明器一个「把话说死」的抓手。

配套的递归函数与模式匹配，让「沿着结构做递归」和「沿着结构做归纳」成为同一条流水线的两个方向。比如定义加法：plus zero m := m，plus (succ n) m := succ (plus n m)——第一行处理桥台，第二行处理后继板。这就是为什么 Lean 能表达「无限」：它不靠直觉，靠一条标准化的预制生产线。

理解了归纳类型，你就拿到了 Lean 世界通向「无限」的钥匙。数学里大量证明之所以能走向无穷，不是因为直觉跳跃，而是因为这类模具备好了每一块板的规格。

AI 定理证明——为什么社区把工地包给机器人

AI 要学造桥，最怕什么？没有明确验收反馈。你说机器人铺错了，得有个监理立刻指出。Lean 恰好提供了这样的反馈环境：每一步 tactic 都有机器验证结果，目标状态立刻变化，这简直是强化学习天生的训练场。相比之下，如果让 AI 学「读自然语言论文并判断证明对不对」，反馈既延迟又不确定。

正是这个原因，AI 定理证明社区近年大量围绕 Lean 展开。GPT-f 用预训练模型生成 tactic 序列，Lean 的检查器负责给每一步打分；LeanCopilot 直接在编辑器里给数学家提供自动补全和 auto 策略；还有用蒙特卡洛树搜索在 Lean 验证反馈下搜索证明树的系统。Mathlib 统一数学库则成了 AI 的「语料库」，模型可以从中模仿人类数学家积累的成千上万条证明模式。

对比 Coq 和 Isabelle：Coq 同样强大，但它的数学库不像 Mathlib 那样统一，学习曲线也更陡；Isabelle 的自动化工具链（如 sledgehammer）很出色，但它的脚本语言与目标语言分离。Lean 主张代码与证明一体化、内核小、元编程能力内置，因此被不少研究者当作「AI 原生」的定理证明平台。这种偏好已经形成气候——Leandojo 等基准测试都建立在 Lean 之上。

对 AI 来说，Lean 是一个规格统一、验收迅速的工地；对数学家来说，它又是一本能自动查错的工程手册。这双重身份，让 Lean 成为连接人类数学与机器推理的那座桥。

AI 应用场景

Python 演示

# -*- coding: utf-8 -*-"""迷你 Lean 证明引擎:用 intro 与 exact 两个 tactic 搭一座逻辑桥""" class Formula:    """一个朴素的逻辑公式:atom / arrow / conj"""     def __init__(self, kind, left=None, right=None, name=""):        self.kind = kind   # atom 原子, arrow 蕴含, conj 合取        self.left = left        self.right = right        self.name = name     def show(self):        if self.kind == "atom":            return self.name        if self.kind == "arrow":            return "(%s -> %s)" % (self.left.show(), self.right.show())        return "(%s /\\ %s)" % (self.left.show(), self.right.show())  def atom(name):    return Formula("atom", name=name)  P = atom("P")Q = atom("Q") # 目标:P -> Q -> P (对应 Lean 中 theorem tP : P -> Q -> P)TARGET = Formula("arrow", P, Formula("arrow", Q, P))  class State:    """证明状态:已知前提 + 当前目标"""     def __init__(self):        self.hyps = []   # [(名字, 公式)]        self.target = TARGET  def do_intro(st, steps, name):    """tactic intro:目标 A->B 时,把 A 收入前提,目标收窄为 B"""    t = st.target    if t.kind != "arrow":        return False    st.hyps.append((name, t.left))    st.target = t.right    steps.append("intro " + name)    return True  def do_exact(st, steps, name):    """tactic exact:前提中找到与目标相同的公式则收工"""    for (nm, f) in st.hyps:        if nm == name and f.show() == st.target.show():            steps.append("exact " + name)            st.target = None            return True    return False  def prove():    st = State()    steps = []    ok = do_intro(st, steps, "hP")    ok = do_intro(st, steps, "hQ") and ok    ok = do_exact(st, steps, "hP") and ok    return steps, ok  if __name__ == "__main__":    steps, ok = prove()    print("证明过程(与 Lean 的 tactic 一一对应):")    for s in steps:        print("  " + s)    print("证明结果:", "桥已连通,目标清空!" if ok else "目标未完成")

1. class Formula把逻辑公式建模成树，kind 标记原子命题、蕴含、合取，对应 Lean 中的类型构造器。
2. st.hyps.append((name, t.left))把箭头左侧的前提收入上下文，这正是 Lean 中 intro 的语义：目标从 A→B 收窄成 B。
3. if nm == name and f.show() == st.target.show()exact 要求前提名与目标完全一致，像监理核对桥板编号与图纸编号完全对应。
4. ok = do_intro(...) and ok从后往前组装战术序列，保证每一步都成功后才算通过验收。
5. prove()完整证明流程：两次 intro 收下 hP、hQ，最后 exact hP 命中目标，桥板铺完。

常见误区

面试题