Introduction to Lean for Programmers

证明助手简介

我是一名从数据科学转型而来的程序员，每天都在与机器学习算法打交道。我既被它们看似神奇的表现所吸引，也被其背后的数学原理深深吸引。打开任何一个机器学习库，你都会发现涉及矩阵分解、卷积、高斯曲线等的数学技巧。而这些技巧又建立在更基础的公理和规则之上，例如函数应用和逻辑。

在我学习这些基础概念的过程中，我收集了一整书架的数学书籍，其中许多如今已蒙尘。我还报名参加了开放大学，通过 Zoom 上课，学习语法与公理，然后学习如何将它们组合起来构建定理。

这个主题非常迷人：公理就像棋盘上的棋子和合法走法，而定理则是合法的棋局，有些比其他更有趣。证明一个定理，意味着将游戏过程回溯到足以说服玩家它可达成的程度；或者通过指出其不可能性来证伪它。例如：“_两个象都在白格上，而象永远无法移动到不同颜色的格子上_。”

但在实际操作层面，这些课程枯燥乏味。我被提供 PDF 文件，需要手工解答，然后在线提交手写作业的扫描件。当我用铅笔在纸上涂写、艰难完成课程作业时，我产生了两个洞见：

1. 构建证明就像编程。
2. 我不可能在如此“20世纪早期”的条件下与数学互动。我需要一个 IDE，具备类型提示、语法高亮和描述性错误信息，并能与之交互式协作。

我的想法并不新颖。第一个观点被称为 Curry-Howard 对应关系，下面将加以解释；第二个观点正是 Lean 等证明助手及其 IDE 扩展（通常是 VS Code 扩展）所追求的目标。

交互式证明助手 vs 自动定理证明器

像 Lean 的内核这样的定理校验器可以判断表达式是否语法正确、步骤是否合法、最终结论是否有效。交互式证明助手在此基础上进一步帮助你构建证明并推荐步骤。自动定理证明器（ATPs）则试图利用 AI 技术自行寻找证明。Lean 本身是一个证明校验器和助手，但它与生成式 AI 结合后，能有效充当 ATP。

Terence Tao 在他的 YouTube 频道 上使用 Lean 4 和 GitHub Copilot 直播 AI 辅助的证明过程。大多数标题为“_AI 刚刚解决了某个已存在 X 年的开放问题_”的新闻，很可能都是用 Lean 形式化完成的（示例 1、示例 2 和 3）。AI 项目与基准测试，如 LeanDojo、miniF2F、ProofNet、PutnamBench、FormalMATH，均使用 Lean。OpenAI 和 Meta 已训练出可使用 Lean 的模型，而 DeepMind 的 AlphaProof 更是借助它赢得了 国际数学奥林匹克竞赛银牌。

DeepMind 的 AlphaProof 核心推理组件。a：证明代理观察初始的 Lean 战术状态，b：证明网络（受 AlphaZero 启发的 3b transformer 模型）生成一组有前景的战术，c：树搜索利用证明网络的输出引导其对潜在证明路径的探索。这是一个神经符号系统，大量架构沿用了 AlphaZero 下围棋的设计。摘自 Nature 文章，采用 Creative Commons 许可。

目前已有大量 Lean 的指南和教程 及活跃社区，但其目标受众似乎并非其他编程语言的资深开发者。我在脑海中解析 Lean 语法时感到困难，学习过程中也意识到自己正走在一条尚未铺就的路上。希望接下来的章节能为你指引这条道路。

Curry-Howard 对应关系

让我们从一个简单的逻辑定理开始，这可能是你在本科逻辑课上需要证明的内容：

(P → Q → R) → (P ∧ Q → R)

其中，运算符 → 表示逻辑蕴含，但在证明与计算机程序之间的 Curry-Howard 对应关系中，它可以被理解为函数。∧ 是逻辑“与”。用通俗的话说，我们的问题是：_“如果我有一个函数，给定 P 后能产生一个从 Q 到 R 的函数，那么当我已经拥有 P 和 Q 时，我是否能得出 R？”_

注意：(P → Q → R) 是一个“柯里化函数”（Haskell Curry 也得为此负责），其语法等价于 (P → (Q → R))。从编程角度看，它是一个返回另一个函数的函数，之后可以像 foo(bar)(baz) 这样调用。逻辑上，它等价于 foo 接收一个包含 bar 和 baz 的元组 foo((bar, baz))，但这一点正是我们试图证明的。同样，整个语句也可以写作 (P → Q → R) → P ∧ Q → R。

让我们用一个具体例子来理解：假设我有一台自动售货机，它接受一枚硬币 (P)，返回一份速食面 (Q → R)，而这份速食面在加入热水 (Q) 后，会产出面条 (R)。这意味着我可以构建一个系统，输入同时包含硬币和热水 (P ∧ Q)，就能输出面条。

杯面自动售货机。这些机器已为你提供热水。维基媒体基金会。

如果你被要求作为一名程序员证明这是可行的，你可能会倾向于编写一个符合该场景的函数。在 TypeScript 中，我们可以这样写：

在 TypeScript 播放器 中尝试，任何修改都会导致类型错误。

通用且简化后的版本（播放器）：

我们定义了一个函数——即我们的定理——它接收一个柯里化函数 (P → Q → R) 作为参数，并输出一个接收积类型 P ∧ Q 并返回 R 的函数，即 (P ∧ Q → R)。这个函数充当了“见证者”，证明该逻辑定理成立。该证明看起来是合理的，并且甚至满足了用 TypeScript 表达原始定理的类型：

让我们更进一步：这个证明之所以成立，正是因为它满足了类型。命题即类型，证明即这些类型的项。我们还看到，合取 ∧ 是积类型/元组，而逻辑蕴含 Q → R 是函数 (q: Q) => R。箭头在语法和语义上都是等价的。

让我们在 Lean 中实现它：

你可以在 Lean 播放器 中试用。

example 是一种仅用于检查类型的匿名声明方式（不同于 theorem 关键字），其类型（冒号 : 到定义 := 之间的部分）就是我们的定理。当一个定义“ inhabit ”这个类型时，证明就完成了。正如函数式编程中的惯例，函数应用仅用空格表示：最基础的操作被映射为语言中最基本的运算符。P ∧ Q 是一个积类型/元组，其成员通过 .left 和 .right 访问。

注意，类型和实现几乎完全一致——仅凭类型就足以推导出代码。事实上，给定一个类型签名，你可以使用 Loogle 在 Lean 的库中搜索匹配的定义。

#### 其他 Curry-Howard 对应关系

| 逻辑/Lean | 类型形式 | TypeScript 近似 | | --- | --- | --- | | P ∧ Q | 积类型 | [P, Q] 或 { left: P; right: Q } | | P ∨ Q | 和类型 | P | Q * | | P → Q | 函数类型 | (p: P) => Q | | True | 单元类型 | undefined 或 null | | False | 空类型 | never | | ¬P | 到空类型的函数 | (p: P) => never | | P ↔ Q | 函数对 | [(p: P) => Q, (q: Q) => P] | | (P ∧ Q) → R | 来自积类型的函数 | (pq: [P, Q]) => R | | P → Q → R | 柯里化函数 | (p: P) => (q: Q) => R |

• 更好的和类型是带标签的联合类型：{ tag: “left”; value: P } | { tag: “right”; value: Q }

你尚未见过的内容

依赖类型

让我们看一个更复杂的类型：

它的含义是：“对于所有自然数 x（∀），0 小于或等于 x。” 我们首先注意到的是 Unicode 数学符号；这些符号可以在 IDE 中通过 \forall 自动补全，或直接用 ASCII 关键字 forall 替代。

这看起来不像一个类型。该类型依赖于 x 的值——这通常是像 Zod 这样的复杂验证库才具备的特性，而非 TypeScript 这样的静态类型检查器。这是一种“依赖”于值的类型。然而，Lean 的类型并不像 Zod 那样依赖运行时检查；它仍然是一个类型，尽管更复杂。这正是阅读 Lean 语法时容易产生困惑的来源。

艺术家对可观测宇宙的对数尺度构想，太阳系位于中心。维基媒体基金会。

宇宙层级

在游乐场或IDE中，我们可以使用 #check 检查项的类型：

现在我们来检查 Nat 的类型：

Nat 的类型是 Type。但为什么止步于此？

Type 是 Type 1 的类型，依此类推。这表明在 Lean 中，类型与项之间并不存在严格的语法区分。类型本身就是具有自身类型的项，层层堆叠如洋葱——这些层被称为“宇宙层级”。3 是类型为 Nat 的项，Nat 是类型为 Type 的项，Type n 的类型是 Type (n+1)，以此类推。

Lean 必须跟踪宇宙层级以避免理发师悖论：“一个理发师只为那些不给自己刮胡子的人刮胡子，那么理发师是否给自己刮胡子？” 通过类型宇宙，理发师是一个过程，其类型只能作用于来自更低层级宇宙的元素，而不能作用于自身层级的元素，包括它自己。这避免了可能导致不一致的自指悖论。不一致意味着我们可以证明 False 为真，并由此证明所有命题都为真。

命题

让我们尝试一个更复杂的类型：

用通俗英语表达：“这是真的吗？对于任意自然数 x、y、z 和 n，若已知 n > 2 且 x * y * z ≠ 0，我们能否推出 xⁿ + yⁿ ≠ zⁿ？”

这就是费马大定理，费马声称他的证明无法写在页边空白处，该定理困扰了数学家长达358年。该定义使用了 sorry，它是一个未完成证明的占位符。代码可以编译，但会提示你：declaration uses sorry`。这就像使用 TypeScript 的 any` 来抑制类型错误，但审查者可能会注意到并要求你修复该 lint 错误。提供这个证明就是你的“目标”。

让我们回到一个更简单的问题：

这太荒谬了。我该如何定义一个类型为 2 + 2 = 4 的项？

让我们先查看其类型：

该类型是一个 Prop，即命题的缩写。命题是一个可以为真或假的陈述。如上所述，在 Curry-Howard 对应中，命题是一个类型，而证明则是该类型的项或程序。如果该类型“有 inhabitant”，则命题为真；否则为假。Lean 并不会在计算意义上将命题“解析”为布尔值 true 或 false；我们只是说它是“真”或“假”。使用 Lean 作为证明助手，意味着我们主要处理命题。

在后台，Lean 的类型检查器会为你将此类型归一化为 4 = 4，但不会进一步处理。我们只需提供一个能 inhabit 这个归一化类型的项即可。我们使用 rfl 实现这一点，它是从 `Prelude` 包自动导入到你命名空间中的一个构造器。

这可行。这是一种声明式语法，用于通过自反性断言 2 + 2 = 4 为真。为了理解为何可行，我们检查其类型：

这些是泛型，按惯例使用希腊字母。大括号表示 Lean 会为你自动推断它们。

rfl.{u} 是函数名称及其宇宙层级（你所处的类型洋葱层）。（{α : Sort u} 表示 α 是位于宇宙层级 _u_ 的类型，与“可排序”无关，它只是“sort” u。）{a : α} 表示 a 是类型为 α 的项，而 rfl 的类型最终是命题 a = a。在我们的情形中，α 是 Nat，a 是 4，rfl 的类型是 4 = 4，与 Lean 上述归一化后的类型匹配。我们找到了 2 + 2 = 4 的一个 inhabitant，从而通过自反性证明了该命题。

教练与团队讨论战术。_DoD 图片由一级通信专家 Daniel Hinton 提供。DVIDS。公共领域。_

战术

之前我们仅通过函数应用解决了自动售货机的例子，但 Lean 中还有许多更有趣的原语。在 Lean 中，你可以用 by 开始你的证明，从而激活“战术”模式：

这使你可以逐步构建证明，同时 IDE 的右侧窗格（InfoView）会逐步显示你的局部假设和目标，以 ⊢ 标记。战术是宏和语法糖的组合，用于解决类型检查内核的证明状态。它们帮助你以分析性和声明性的方式思考并解决目标。这是一种在函数式语言内部运行的命令式解决方案，运行在单子之上。

你必须熟悉战术，就像学习 SQL 的人要熟悉 GROUP BY、PIVOT 和 LEFT JOIN 等分析结构一样。移除 sorry 将在 InfoView 中显示当前状态和目标：

我们有一个目标需要证明。Coin 和 HotWater 是命题。Noodles 是一个未知的 sort ?u.29，一个尚未分配的宇宙层级的随机 ID。我们的目标是构造一个证明：(Coin → HotWater → Noodles) → Coin ∧ HotWater → Noodles。

让我们使用战术 intro 引入一个假设到作用域中。它会自动捕获输入类型 (Coin → HotWater → Noodles)——这是我已有的一个证明：

InfoView 将刷新并显示更新后的局部假设和目标：

除了 Coin、HotWater 和 Noodles，我们现在还有一个局部假设（或前提）：noodleVendingMachine，其类型为 Coin → HotWater → Noodles（一个柯里化函数）。我们的新目标是构造 Coin ∧ HotWater → Noodles。

让我们引入另一个变量，它将自动捕获下一个类型为 Coin ∧ HotWater 的假设：

现在的 InfoView 显示：

现在我们只需要使用我们的策略工具箱和局部作用域中的假设来返回 Noodles。我们有一个柯里化的函数 noodleVendingMachine 和一个乘积类型（元组）coinAndHotWater。让我们从 coinAndHotWater 中应用 Coin 和 HotWater 到 noodleVendingMachine：

当我们要返回确切的类型时，策略 exact 充当了返回关键字。.left 和 .right 是乘积类型/元组 coinAndHotWater 的元素，我们按顺序将其应用到柯里化函数 noodleVendingMachine。记住空白字符就是函数应用。

InfoView 显示：

这可以泛型地写成：

满足了我们上面的原始定理 (P → Q → R) → (P ∧ Q → R)。

一些策略帮助将目标分解为更小的义务，比如 `intro`、`cases`、`constructor`、`apply` 或 `refine`。其他策略使用等价性的假设重写表达式，比如 `rw` 或 `simp`。还有一些策略通过计算或代数操作规范化表达式，比如 `rfl` 和 `ring`。还有一些提供针对性的自动化：`linearinth`、`omega`、`aesop`。请查阅策略参考。

用策略思考是一种优雅的技能，只能通过经验获得。借用前面的一个类比，就像数据分析师调出正确的分析函数并轻松清理、丰富和汇总表格——或者高级软件工程师将正确的 Bash 命令管道连接在一起或识别出最适合工作的最简洁的设计模式。

定理证明器的总体愿景

莱布尼茨的机械计算器（1671年）。第一台能够执行加减乘除运算的计算器。维基媒体基金会。

莱布尼茨梦想着一种通用的形式思维语言（_Characteristica universalis_）与一台机械计算器（_Calculus ratiocinator_）配对，通过转动曲柄就能证明所有定理和哲学论证。希尔伯特问道："这可能吗？"——直到去世都确信"_没有什么是我们不能知道的。_" 这被认为是"_数理逻辑的主要问题_"和"_数学最一般的问题_。" 哥德尔思考了这个问题并证明了有些真理无法被证明，而丘奇和图灵各自独立地证明了"你经常会永远转那个曲柄"，这一过程可以说开创了计算机科学领域。用前面的象棋类比来说，自动定理证明就像搜索游戏树寻找获胜位置，但数学有一个无限大的棋盘，所以搜索可能永远不会结束——有些走法是"不可判定的"。然而，我们仍然可以检查一个走法是否合法，这就是我们现在使用证明助手所处的位置。

1956年，伯特兰·罗素写了一封关于逻辑理论家的信，该程序自动证明了《数学原理》中的定理，有时被称为第一个 AI 程序：

"我希望怀特海和我在浪费十年时间手工完成之前就知道这种可能性。我完全愿意相信演绎逻辑中的一切都可以由机器完成。"

结论

Lean 有陡峭的学习曲线，部分原因是其语法和必须学习的策略使用。然而，与 Lean 斗争会带来回报：你在学习数学。类型、宇宙、策略、定理和证明不是另一个编程语言的怪癖，而是数学家和逻辑学家几代人以来一直在思考的概念。它们不是需要记忆的无用事实，而是像欧几里得一样古老、像我们证明的定理一样永恒的思维模式。

在熟悉基础知识后，你可以尝试深入更高级的主题，例如通过 _Lean 中的数学_ 学习离散数学、线性代数、微分微积分和拓扑学中的问题。或者，从零开始（ literally）深入探究基础，通过陶哲轩的 《分析 I》的 Lean 伴侣。Lean 的协作库 Mathlib 已经包含了 160 万行形式化数学内容，你可以借助它连接到数学的各个分支。