第 1 章：逃离焦油坑——为什么我们需要 Lean4？

你写了一个函数。你为它写了单元测试。你为那些单元测试写了边界条件。你把测试覆盖率推到了98%，然后在代码审查时得意地把这个数字贴在了 Pull Request 的描述里。

三天后，生产环境炸了。

错误信息指向一个你从未想过会发生的输入组合。你的测试覆盖了你能想到的所有情况，但 bug 来自一个你根本没想到的情况。你盯着屏幕上的堆栈追踪，突然意识到一个令人不安的事实：测试只能证明你测过的路径是对的。它无法证明那些你没测过的路径不会出错。

这就是焦油坑。

100% 覆盖率的谎言

如果你是一个有几年经验的 Python 程序员，你一定经历过这种场景。CI 管线里所有的绿色对勾像是一排整齐的士兵向你敬礼，告诉你一切安好。但你心里清楚，这排士兵守卫的只是你已知的城门。那些你没画在地图上的暗道，没有任何人在巡逻。

Python 的类型系统是一面纸糊的盾牌。x: int 这行 Type Hint 写在那里，看起来像一个承诺，但 Python 解释器根本不会去检查这个承诺是否被兑现。你可以在运行时往 x 里塞一个字符串，解释器不会眨一下眼睛——直到这个字符串在某处参与了一次加法运算，然后抛出一个 TypeError，此时程序已经在生产环境中运行了七十二个小时。

MyPy 和 Pyright 改善了这个局面，但它们本质上仍然是静态分析工具在动态语言上打的补丁。它们能告诉你"这里的类型不匹配"，但它们无法告诉你"这个函数对于所有可能的输入都会返回正确的结果"。

这两者之间的鸿沟，就是测试和证明之间的鸿沟。

那个拥有双重人格的家伙

Lean4 是一个奇怪的存在。

它是一门编程语言。你可以用它定义数据结构、编写函数、处理输入输出、编译生成可执行文件。它有着纯正的函数式血统——没有可变状态、没有副作用（至少在纯粹的逻辑世界里如此）。如果你写过 Haskell，你会觉得它像一个更年轻、更实用的同胞兄弟。

但 Lean4 同时也是一个定理证明器。

这意味着你不仅可以用它写出一个排序算法，你还可以在同一套系统里，用数学语言写下一条声明——"这个排序算法对于任何输入列表，输出的列表都是有序的，而且包含且仅包含原列表的所有元素"——然后让编译器去验证这条声明是否为真。

不是用一百个测试用例去"大概率"验证。而是用数学证明去"绝对"验证。

编译通过的那一刻，你不是在说"我测了很多情况都没出错"。你是在说"我已经数学证明了，这件事在所有情况下都不可能出错"。

这就是从测试到证明的维度跃迁。

"我用 TypeScript 不就行了？"

如果你心里正在嘀咕这句话，那说明你已经嗅到了方向，但还没看到全貌。

TypeScript、MyPy、Java 的泛型——这些类型系统确实比 Python 的裸奔强了不少。它们能在编译时捕获类型不匹配的错误。但它们的能力止步于此。它们能告诉你"这个函数接收一个数组并返回一个数组"，但它们无法表达"返回的数组与输入数组是同一组元素的重新排列"。

这种更强大的表达能力来自一个叫做"依赖类型"的概念。在依赖类型系统中，类型可以依赖于值。你不只是说"这个函数返回一个列表"，你可以说"这个函数返回一个长度等于输入列表长度的有序列表"。这个约束不是写在注释里的美好愿望，而是刻在类型系统里的铁律——如果你的实现违反了它，代码根本无法编译。

Lean4 拥有完整的依赖类型系统。TypeScript 没有。Java 没有。Haskell 的某些扩展在朝着这个方向走，但远没有 Lean4 走得彻底。

所以，不，TypeScript 不行。它只是在焦油坑外面修了一条人行道。而 Lean4 给了你一架直升机。

AI 时代的新焦虑

让我们暂时把目光从语言设计转向另一个正在塑造我们工作方式的力量：大模型。

你已经用过 Copilot 或 Gemini 来写代码了。它们让你写得更快了——这不是问题。问题在于，它们也让你写得更多了。更多的代码意味着更大的攻击面。而你对这些代码的理解程度，往往远低于你自己一行行敲出来的代码。

AI 生成的代码就像一个口才极佳的辩护律师递给你的辩护词。措辞漂亮，逻辑看起来天衣无缝。但你真的逐字核实过每一条引用吗？你真的确认过每一个论据的来源吗？

在动态语言的世界里，你没有办法核实。你只能写更多测试——但我们已经知道了，测试覆盖的永远只是你已知的领地。

而在 Lean4 的世界里，你拥有一个冷酷无情的法官：编译器。你可以把 AI 辩护律师生成的代码和证明扔给这个法官，让它逐行审查。法官不讲情面，不收贿赂，不被花言巧语打动。如果证明有任何漏洞——哪怕只是逻辑推理中的一个微小缝隙——它就会当场驳回。

这就是 Lean4 在 AI 时代的独特价值：它不是用来替代 AI 的，而是用来审判 AI 的。

不是替代，而是升维

让我在这一章的结尾说清楚一件事：这本书不是要说服你抛弃 Python。

Python 是一把出色的瑞士军刀，而你将来写的绝大多数代码仍然会是 Python 或者 JavaScript 或者 Go。Lean4 不会取代它们。

但每一个工程师的职业生涯中，都会遇到几次这样的时刻：你需要写的那段代码，如果出错了，代价是灾难性的。可能是一个加密协议的核心逻辑。可能是一个金融交易引擎的清算算法。可能是一个自动驾驶系统的决策模块。在这些时刻，"我测了很多情况都没出错"不够。你需要"我已经数学证明了它不可能出错"。

这就是形式化验证的疆域。这就是 Lean4 的主场。

现在，让我们走进法庭。

打开你的浏览器，进入 GitHub Codespaces。在下一章开始之前，我们需要先做一件事：为你的 AI 辩护律师戴上镣铐。

参考资料

引用来源表

原始链接列表

https://leanprover.github.io/theorem_proving_in_lean4/
https://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html
https://peps.python.org/pep-0484/
https://github.com/aws/s2n-tls
https://hacl-star.github.io/HaclValeEverCrypt.html

第 2 章：驯服幻觉——Vibe Coding 的"排雷指南"

让我们做一个实验。

打开 Lean4 Web——一个不需要安装任何东西、在浏览器里直接运行的 Lean4 在线编辑器。然后打开 Chrome 的 Gemini 侧边栏（点击右上角的 G 图标），把两个窗口并排放好。

现在，在 Gemini 侧边栏的对话框里输入："请用 Lean4 证明：对于所有自然数 n，n + 0 = n。"

如果你运气好，Gemini 会给出一段看起来像模像样的代码。把它复制到左侧的 Lean4 Web 编辑器。

两种情况都可能发生：代码直接通过，或者出现红色报错。这两种情况都很有价值——前者让你体验成功的闭环，后者才是真正的学习开始。

Lean4 Web + Gemini：你的三栏工作台

在深入讲方法论之前，让我先介绍这个工作流的物理设置。

把你的 Chrome 浏览器分成三个区域：

左侧是 Lean4 Web（或你本地的 VS Code + Lean4 插件）。这是你的代码编辑区。中间偏右是 Infoview 面板——它在网页版中默认显示在编辑器右侧，实时展示当前的证明状态。最右边是 Chrome 的 Gemini 侧边栏。

这种三栏布局不是偶然的。它精确地对应了我们的法庭隐喻：你写策略（左），法官实时更新裁决（中），辩护律师随时待命（右）。

Gemini 侧边栏的一个特别优势是：它能直接感知你正在当前页面上做什么。当 Lean4 Web 报错时，你可以直接向侧边栏里问"这个错误是什么意思？"，Gemini 会读取页面上下文并给出解释。这比在两个独立窗口之间复制粘贴报错信息要高效得多。

为什么 AI 在 Lean4 面前有时候是个骗子

大语言模型的本质是一台概率预测机器。它不理解逻辑，它理解的是统计分布：在训练数据中，这个 token 之后出现那个 token 的概率最高。

当你让它写 Python 代码时，它表现不错。因为 GitHub 上有数以亿计的 Python 文件，统计分布足够稠密。当它犯错时，错误往往小而局部，你凭经验就能发现。

Lean4 的情况曾经（在几年前）要糟糕得多——互联网上的 Lean4 代码量极少，AI 会频繁产生幻觉。现在的情况已经好了很多：随着 Mathlib 和 Lean4 社区的繁荣，主流大模型对 Lean4 的理解能力持续提升，Gemini 在处理基础到中等难度的证明时通常表现相当不错。

但有一件事不会改变：Lean4 的证明是二值的——要么完全正确（编译通过），要么完全错误（编译失败）。没有中间地带。再强的 AI 生成的代码，也需要通过这个冷酷无情的数学检验。随着时间推移，AI 能生成的代码越来越接近正确，但编译器的终极裁决权永远不会转让。

所以，即使 AI 越来越强，你仍然需要本章介绍的工作流——它会随着 AI 能力的提升而变得更流畅，但核心结构保持不变。

不要只是复制粘贴：CoT 模板的真正价值

我见过太多人用 AI 学 Lean4 的方式：问 AI 要代码，复制，粘贴，过了就继续，报错了就再问一遍。

这是在浪费一个绝佳的机会。

让我介绍一个不同的 Prompt 模板：

"我需要在 Lean4 中证明以下命题：[具体命题]。请不要直接给我完整的证明代码。请按以下步骤进行：第一，用自然语言描述你的证明策略（思路大纲）。第二，列出你计划使用的关键引理和定理，并说明每一个引理的名称和用途。第三，如果需要辅助引理，请先给出辅助引理的陈述（不含证明）。第四，最后再给出完整的 Lean4 代码。"

这个模板的价值并不只在于"约束 AI 不能乱说"。它的更深层价值在于：你被迫跟着 AI 的思路走一遍。

当 AI 在第一步描述证明策略时，你要读懂它的思路。当它在第二步列出引理时，你要问自己"这个引理是干什么的？"。当你最终拿到代码时，你不是在面对一个黑盒，而是在验证一个你已经理解了结构的论证。

这就是 Chain-of-Thought 教学法的精髓：你和 AI 一起经历了推理过程。如果证明后来出错了，你知道从哪里开始排查。如果证明通过了，你能解释每一步为什么这么做。

这才是学习，不是复印。

红绿灯闭环法则

即便用了上面的 Prompt 模板，AI 生成的代码有时会无法通过编译。这不是失败——这是系统设计的一部分。

把这个循环叫做"红绿灯闭环"：

第一步，生成。 用 CoT Prompt 模板让 Gemini 产出证明草稿。

第二步，编译。 把代码粘贴到 Lean4 Web 的编辑器中。看 Infoview 面板。看报错信息。

第三步，投喂报错。 把编译器的完整错误信息原封不动地告诉 Gemini。你还可以直接在 Chrome 侧边栏里问"这个错误是什么意思？"——Gemini 能读取页面上下文，通常能给出清晰的解释。

第四步，修正。 根据 Gemini 的解释，理解错误，然后让它给出修正方案。把修正后的代码再次粘贴。

重复。每一轮循环，你对这个证明的理解都在加深。几轮之后，代码通过编译。Infoview 面板清空。寂静。

这个工作流的精髓：AI 负责创意和初始推理，编译器负责绝对裁决，你负责理解两者之间的对话。

你不需要自己从零想出证明的每一步。但你需要真正理解每一步是什么意思。这个区别，在你面对更难的问题时将会决定你能走多远。

一个完整的示范

让我展示一次真实的 CoT 工作流。目标命题：∀ (n : Nat), 0 + n = n。

你发给 Gemini 的 Prompt（按上面的模板）。Gemini 的回答大致是：

第一步，证明策略：对 n 做数学归纳法。基础情况：n = 0 时，0 + 0 = 0（根据加法定义）。归纳步骤：假设 0 + n = n 成立，证明 0 + succ(n) = succ(n)（根据加法的递归定义和归纳假设）。

第二步，关键引理：Nat.add_succ（加法对后继的递归定义：m + succ n = succ (m + n)）。

第三步，没有需要额外证明的辅助引理。

第四步，代码：

theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    rw [Nat.add_succ, ih]

你拿到代码了。但更重要的是，你拿到了思路。你知道为什么要用 induction，你知道 Nat.add_succ 是用来做什么的，你知道 ih 是归纳假设的名字。

把代码粘贴进 Lean4 Web。如果出错，把报错给 Gemini 问"这是什么意思"。如果通过，尝试自己用同样的思路证明一道变形题：∀ (n : Nat), n + 0 = n（注意是对第二个参数加零，结果不同）。

你已经上路了。

"等 AI 更强了就不需要这套了"

越来越强的 AI 不会让这套工作流过时，只会让它运转得更顺畅。

原因在于：编译器的数学验证是绝对的。无论 AI 多么聪明，它生成的证明都必须经过编译器的检查——不可绕过，不可说服，不可贿赂。

更重要的是，这套工作流的核心价值不在于"帮你生成通过编译的代码"，而在于"帮你理解证明的逻辑结构"。即使有一天 AI 能百分之百生成正确的 Lean4 证明，你仍然需要理解那个证明，才能在它的基础上继续工作、才能在它出错时知道如何修复。

律师帮你写了一份完美的合同不意味着你不需要读懂合同。

在下一章，我们正式进入法庭——但首先，我们需要先学会看懂法庭上使用的语言。

参考资料

引用来源表

原始链接列表

https://live.lean-lang.org/
https://arxiv.org/abs/2201.11903
https://leanprover.github.io/lean4/doc/
https://gemini.google.com/

第 3 章：Hello, Goal！第一场逻辑诉讼

法庭开庭了。

打开 Lean4 Web，把页面顶部下拉框选为"Latest Mathlib"——这样你才能用到最完整的数学库。你会看到一个分成两半的界面：左边是代码编辑区，右边是 Infoview 面板。

在写第一行 Lean4 代码之前，我们先来拆解这门语言的语法。你是 Python 程序员，你见过的等号只有一种意思，你见过的冒号只有两种用法。在 Lean4 里，这些熟悉的符号都有了新的角色。搞清楚它们，是走进法庭的第一步。

解剖一行 Lean4 代码

在编辑器里输入这行代码：

example : 1 + 1 = 2 := by
  rfl

这不是 Python。每一个字符都在做特定的事情。让我们把这行代码像化学方程式一样拆开。

example 是一个关键词。它的意思是"我要声明并证明一个命题，但我不给它起名字"。如果你想给命题起名字（以便后续引用），就用 theorem 或 lemma 替代 example。对于练习来说，example 就够了。

:（第一个冒号） 是"其类型为"的意思。在 Lean4 里，冒号是一个极其重要的符号——它把一个名字和它的类型（或一个命题和它的证明）连接起来。example : 1 + 1 = 2 的意思是"这是一个类型为 1 + 1 = 2 的东西"。在形式化验证的世界里，命题就是一种类型（你在第五章会深刻理解这一点）。

1 + 1 = 2 是命题本身——你要证明的东西。注意这里的 = 是数学等号，是你要证明的断言，不是赋值。

:=（冒号等号） 是"定义为"的意思。它比 Python 的 = 更接近"等价于"，但专门用于定义一个值、函数或证明。example : P := [证明] 的意思是"类型为 P 的那个东西，其具体内容是这个证明"。

by 是进入"策略模式"的开关。Lean4 有两种写证明的方式：直接写出证明项（一种程序化风格），或者用 by 进入交互式策略模式，一步步告诉编译器怎么证明。本书绝大多数证明都用 by 模式——它更像对话，也更适合入门。

rfl 是你的第一个策略（tactic）。它缩写自 reflexivity（自反性）。它的意思是："等号两边，如果化简后是完全相同的东西，那等式自然成立。"编译器会独立计算 1 + 1，得到 2，确认两边相同，接受这个证明。

缩进 是有意义的。by 之后换行，策略代码需要缩进（至少两个空格或一个 Tab）。和 Python 一样，Lean4 用缩进来表示代码块的归属。

把这行代码放在一起再读一遍："example（声明一个无名命题），其类型是 1 + 1 = 2，被定义为（:=）以下用 by 进入策略模式写成的证明：使用自反性（rfl）。"

更多符号解读

你会在后面的章节中频繁见到这些符号，现在先打一个招呼：

++：字符串拼接运算符。"hello" ++ " world" 得到 "hello world"。在 Lean4 中，对于列表来说 ++ 也是拼接。

example : "hello" ++ " world" = "hello world" := by
  rfl

=>（胖箭头）：出现在两种场合。第一，模式匹配的分支里：| zero => 0 表示"如果是 zero，那么结果是 0"。第二，匿名函数里：fun x => x + 1 表示"接受 x，返回 x + 1"。它不是判断相等，也不是 Python 的 lambda x: x + 1，虽然功能类似。

→（箭头，用 -> 或 \to 输入）：逻辑蕴含，也是函数类型。P → Q 的意思既是"如果 P 那么 Q"（逻辑层面），也是"一个接受 P 类型输入、返回 Q 类型输出的函数"（类型层面）。等号一个是赋值（Python 里没有对应的）；两个 == 在 Lean4 里是可判定相等（decidable equality），与数学等号 = 有细微区别。

#check 和 #eval：以 # 开头的命令是"编译器指令"，用于调试和探索，不进入正式证明。#check Nat.add_comm 会让编译器告诉你 Nat.add_comm 的类型（签名）。#eval 3 + 5 会让编译器直接计算并显示结果（8）。

Infoview 面板：法庭的状态屏

右边那个不断刷新的面板就是 Infoview。它是这场逻辑官司的实时状态屏。每次你的光标在 by 块里移动，它都会更新，告诉你：

Context（上下文）：你目前"手里有的东西"——已经引入的假设、变量、已知事实。这些写在横线上方。

Goal（目标）：你"还需要证明的东西"——你的待证目标。写在横线下方，用 ⊢ 符号开头（念"turnstal"，意为"可证"）。

当你在 by rfl 后面，如果 rfl 成功，Infoview 会显示"No goals"——没有待证目标了。寂静就是胜利的声音。

如果 rfl 失败，Infoview 会显示红色错误，告诉你它无法通过自反性关闭这个目标。这是编译器在说：你还没有证完，继续工作。

你的前三场官司

把以下三段代码分别粘贴进 Lean4 Web，观察 Infoview 面板的变化：

第一场：数字等式

example : 1 + 1 = 2 := by
  rfl

没有悬念。1 + 1 化简为 2，两边相同，rfl 胜诉。

第二场：字符串拼接

example : "hello" ++ " world" = "hello world" := by
  rfl

rfl 不在乎是数字还是字符串。两边化简后相同就行。

第三场：函数应用

example : (fun x => x + 1) 3 = 4 := by
  rfl

fun x => x + 1 是一个匿名函数，把它应用到 3，得到 4。编译器化简，rfl 结案。

三场。三次 Infoview 显示"No goals"。你刚刚打赢了三场逻辑官司。

rfl 的边界——预告下一章

但 rfl 不是万能的。试试这个：

example : ∀ (n : Nat), n + 0 = n := by
  rfl  -- 这里会报错！

Infoview 会亮红。因为 n 不是一个具体的数字，编译器不知道该怎么化简 n + 0。rfl 只能处理两边化简后完全相同的情况，而 n + 0 和 n 在 Lean4 内部的表示并不相同——即使对人类来说"显然一样"。

要处理这种涉及变量和量词的命题，你需要归纳法和更强大的策略。但那是后面的事。

现在，你已经认识了法庭的物理空间（Lean4 Web）、学会了读法庭语言（基础语法符号），打赢了三场简单的官司。

在下一章，我们暂时离开证明，做一件实际的事：学会用 Lean4 真正地写程序、做计算。因为在法庭辩论之前，你得先知道这个法庭不只是能讲道理，它还能跑代码。

参考资料

引用来源表

原始链接列表

https://live.lean-lang.org/
https://leanprover.github.io/theorem_proving_in_lean4/introduction.html
https://leanprover.github.io/theorem_proving_in_lean4/tactics.html
https://marketplace.visualstudio.com/items?itemName=leanprover.lean4

第 3.5 章：活着的代码——Lean4 也能跑真实程序

等等，先别急着去法庭。

在开始证明定理之前，有一件事需要澄清：Lean4 不只是一个定理证明器，它是一门完整的编程语言。 你可以用它定义函数、做计算、写 CLI 程序、处理数据。

如果你跳过这一章直接冲进证明，很可能会觉得 Lean4 是个只会讲道理的象牙塔玩具。先让你看到它活生生地跑起来，你才能真正感受到"一门语言既能跑程序又能证明程序正确"究竟意味着什么。

这一章不会要求你证明任何东西。我们只是写代码，只是计算。

Lean4 的变量和赋值：let 绑定

Python 的赋值是这样的：

x = 42
y = x + 1
print(y)  # 43

Lean4 的"赋值"是 let 绑定：

def main : IO Unit := do
  let x := 42
  let y := x + 1
  IO.println s!"{y}"   -- 输出 43

几点区别：

let x := 42 用的是 :=（定义为），而不是 Python 的 =（赋值为）。名字 x 不是一个可以被改变的盒子，它是一个永久绑定到 42 这个值的标签。你不能之后写 let x := 99 来"改变" x——那会创建一个新的 x，遮蔽旧的。

s!"{y}" 是字符串插值的语法，类似 Python 的 f-string。s! 前缀之后用大括号插入变量。

IO.println 是向控制台打印一行的函数。它之所以必须在 do 块和 IO Unit 的环境里，是因为打印属于副作用（我们在第七章详细解释）。

if-then-else：条件判断

Python 里的 if 语句：

def describe(n: int) -> str:
    if n > 0:
        return "正数"
    elif n < 0:
        return "负数"
    else:
        return "零"

Lean4 里的 if-then-else：

def describe (n : Int) : String :=
  if n > 0 then "正数"
  else if n < 0 then "负数"
  else "零"

注意这里 if-then-else 是一个表达式，不是语句。它有一个值——就像 Python 的三元运算符 "正数" if n > 0 else "负数"，但写起来更像普通 if。没有冒号，没有 return，直接返回那个分支的值。

函数的定义语法：def 函数名 (参数 : 参数类型) : 返回类型 := 函数体。

让编译器算一下：

#eval describe 5    -- "正数"
#eval describe (-3) -- "负数"
#eval describe 0    -- "零"

#eval 命令让 Lean4 直接计算并显示结果。这是你的 inspect/REPL。

递归函数：告别 for 循环

Lean4 没有 for 循环。取而代之的是递归。这不是限制，这是设计——递归的结构反映了数据的结构，让证明成为可能。

让我们写一个阶乘函数。Python 版本：

def factorial(n: int) -> int:
    if n == 0:
        return 1
    return n * factorial(n - 1)

Lean4 版本：

def factorial : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

这里用了模式匹配。函数定义的每一行是一个模式 → 结果的分支：

• 如果输入是 0，返回 1
• 如果输入是 n + 1（即任何大于零的数），返回 (n + 1) * factorial n

注意 n + 1 在这里不是表达式，而是模式——它表示"任何可以写成某个数加一的自然数"，同时把那个"某个数"绑定到变量 n。这种写法能保证你覆盖了所有情况，编译器来检查穷尽性。

#eval factorial 5   -- 120
#eval factorial 10  -- 3628800

斐波那契数列

def fib(n: int) -> int:
    if n <= 1:
        return n
    return fib(n - 1) + fib(n - 2)

Lean4 版本：

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib n + fib (n + 1)

n + 2 是一个模式，匹配任何大于等于 2 的数，并把它比 2 小的部分绑定到 n。所以当 n + 2 = 5 时，n = 3，函数递归计算 fib 3 + fib 4。

#eval fib 0   -- 0
#eval fib 1   -- 1
#eval fib 10  -- 55
#eval fib 20  -- 6765

这个实现的效率是指数级的——和朴素的 Python 递归版本一样糟糕。这没关系。后面我们会看到 Lean4 也支持更高效的尾递归版本。现在你需要的只是理解模式匹配和递归的基本语法。

列表操作

Python 里你对列表的很多操作，Lean4 里也有对应的方式：

-- 创建列表
let xs := [1, 2, 3, 4, 5]

-- 获取长度
#eval xs.length    -- 5

-- 映射（对应 Python 的 list comprehension 或 map）
#eval xs.map (fun x => x * 2)    -- [2, 4, 6, 8, 10]

-- 过滤（对应 Python 的 filter）
#eval xs.filter (fun x => x % 2 == 0)  -- [2, 4]

-- 折叠（对应 Python 的 reduce）
#eval xs.foldl (· + ·) 0     -- 15（求和）

fun x => x * 2 是匿名函数。· 是简写，(· + ·) 等价于 (fun a b => a + b)。

这些函数——map、filter、foldl——就是 Python 程序员所熟悉的高阶函数。在 Lean4 里，它们是库函数，不是语言内置的特殊语法。

类型标注：你的 Type Hint 升级版

Python 的类型提示是可选的、不被强制：

def add(x: int, y: int) -> int:
    return x + y

Lean4 的类型标注是强制的、被编译器检查的：

def add (x : Nat) (y : Nat) : Nat :=
  x + y

格式：参数写在函数名后面的括号里，每个参数用 (参数名 : 类型) 表示，返回类型在冒号后面的 : Nat。

如果你漏掉类型，编译器会推断——但最好在学习阶段显式写出来，让 Infoview 帮你确认类型是否与你想的一致：

#check add   -- add : Nat → Nat → Nat

#check 告诉你一个表达式的类型。Nat → Nat → Nat 说的是：add 是一个从 Nat 到（从 Nat 到 Nat 的函数）的函数——即接受两个 Nat 参数、返回 Nat 的函数。

用 #eval 做快速实验

#eval 是你在 Lean4 里的 Python REPL。在写正式代码之前，用它快速验证思路：

#eval 2 ^ 10          -- 1024（2的10次方）
#eval "hello".length  -- 5
#eval [1,2,3] ++ [4,5] -- [1, 2, 3, 4, 5]
#eval Nat.gcd 12 8    -- 4（最大公因数）

把这些都粘进 Lean4 Web 试试。#eval 是即时的——你不需要定义 main 函数或运行整个程序。

现在你知道 Lean4 是活的

你刚才用 Lean4 做了加法、条件判断、递归计算、列表操作。它是一门能做真正工作的编程语言。

下一章开始，我们回到证明的世界——但带着一个新的理解：证明的对象，是真实运行的代码。你不是在证明抽象的数学符号，你是在证明 factorial、fib、add 这些具体函数的行为。

类型即契约，证明即保障——而你保障的，是你刚刚写出来的这些活生生跑起来的程序。

参考资料

引用来源表

原始链接列表

https://lean-lang.org/functional_programming_in_lean/getting-to-know/functions-and-definitions.html
https://leanprover.github.io/lean4/doc/
https://lean-lang.org/functional_programming_in_lean/functor-applicative-monad/functor.html
https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html

第 4 章：谋杀 Mutate——函数式的冰与火

翻开任何一本 Python 入门书，你都会在前五页看到这一行代码：

x = 1
x = x + 1
print(x)  # 输出 2

你从未觉得这有什么问题。变量嘛，变量当然可以变。这就像水可以流、火可以烧一样天经地义。

现在，想象你把这行代码拿给一位数学家看。

她会皱起眉头，盯着 x = x + 1 看三秒钟，然后说："这是一个矛盾。这个等式没有解。你是说 x 等于 x 加 1？那两边同时减去 x，你得到 0 = 1。这是假命题。"

她没有错。在数学的世界里，等号意味着"两边是同一个东西"。x = x + 1 是一条不可能成立的方程。

而在 Python 的世界里，= 从来不是数学等号。它是一条赋值命令——"把右边的值塞进左边的盒子里"。x = x + 1 的意思是"算出 x + 1 的值，然后把旧的 x 扔掉，让它指向新的值"。

这两个世界之间的裂缝，就是你从 Python 跨入 Lean4 时必须跳过的第一道深渊。

数学不能容忍可变状态

Lean4 是一门从数学土壤中长出来的语言。在它的世界里，等号就是数学等号。当你写下 let x := 1 时，x 就是 1，从此直到永远。你不能把它改成 2。你不能"更新"它。它不是一个盒子——它是一个名字，一个绑定在某个值上的标签。

这不是 Lean4 的一个限制，而是它的一个特性。

如果变量可以被修改，那么你在证明中使用这个变量时，你就不知道它当前到底是什么值。它可能在程序的某个角落被悄悄改掉了。整个证明的逻辑基础就会像沙子一样松垮。

不变性是可证明性的前提条件。这是一条没法妥协的铁律。

用 Lean4 的方式思考

让我们看看 Lean4 如何定义最基础的几种数据：

自然数在 Lean4 中不是一个原始概念——它是通过归纳定义构建的：

inductive Nat where
  | zero : Nat
  | succ : Nat → Nat

这段代码说的是：自然数只有两种构造方式。第一种，它是 zero——零。第二种，它是某个自然数的后继 succ n——也就是 n+1。

所以 1 就是 succ zero。2 就是 succ (succ zero)。3 就是 succ (succ (succ zero))。没有黑魔法，没有硬件层面的 32 位整型，就是纯粹的逻辑积木。

这种定义方式一旦理解，你会发现它具有令人惊叹的透明性。你知道自然数的全部——它没有任何隐藏的行为、没有溢出、没有未定义的边界条件。法官可以把它彻底看穿。

告别循环，拥抱递归

在 Python 中，你用 for 循环遍历一个列表、用 while 循环执行重复操作。循环依赖于可变状态——你需要一个计数器或条件变量来控制循环的进退。

在 Lean4 中，没有循环。

取而代之的是递归。要计算一个列表的长度，你不说"从头到尾数一遍"（循环），你说"如果列表为空，长度为零；否则，长度是剩余部分的长度加一"（递归）。

def length : List α → Nat
  | [] => 0
  | _ :: tail => 1 + length tail

这段代码比 Python 的 len() 函数更长，但它有一个 Python 版本永远不可能拥有的优势：编译器可以对它进行结构归纳，证明它对所有可能的列表输入都会终止并返回正确的结果。

没有可变状态。没有副作用。每次调用 length，给定相同的输入，永远得到相同的输出。这就是纯函数。

"那我怎么写有用的程序？"

这是每个从命令式编程语言转过来的人都会问的第一个问题，也是一个绝对合理的问题。

如果变量不能变，你怎么读写文件？怎么接收用户输入？怎么和数据库交互？真实世界的程序充满了副作用——而你刚告诉我 Lean4 不允许副作用。这不是自相矛盾吗？

答案是：Lean4 当然能处理副作用。但它用一种极其精巧的方式把副作用隔离起来，不让它们污染纯粹的逻辑世界。这个隔离机制叫做 IO Monad。

我们将在第七章专门讲解 IO Monad。在那之前，你需要做的事情只有一件：接受在纯粹逻辑的世界里，一切都是不可变的。文件读写、网络请求、用户交互——这些都被关在一个特殊的容器里，不允许泄漏到你的证明和纯函数中来。

暂时把你的 Python 直觉锁进柜子里。在接下来的三章中，你将完全沉浸在这个"没有副作用的真理宇宙"中。

实践：你的第一个递归函数

打开 Lean4 编辑器，定义一个简单的递归函数——对自然数的加法：

def add : Nat → Nat → Nat
  | n, Nat.zero => n
  | n, Nat.succ m => Nat.succ (add n m)

这段代码说的是：n + 0 = n（任何数加零等于自身），n + (m+1) = (n+m) + 1（加法的递归定义）。

编译它。没有红线。

然后试试：

#eval add 3 5  -- 输出 8

编译器不仅接受了你的定义，它还能对这个定义进行计算。更关键的是，在后面的章节中，你将用归纳法针对这个定义进行证明——比如证明 add n m = add m n（加法交换律）。

你刚才写的不是一段"大概正确的代码"。你写的是一个可以被严格审判的数学定义。

从现在开始，你的每一行代码都将承受这种重量。

在下一章，我们将到达全书的智力巅峰。如果你一直觉得"命题"和"程序"是两个完全不同的宇宙——准备好，因为它们即将在一个叫做 Curry-Howard 同构的定理面前合二为一。

参考资料

引用来源表

原始链接列表

https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html
https://lean-lang.org/functional_programming_in_lean/
https://leanprover.github.io/lean4/doc/

第 5 章：天外飞仙——Curry-Howard 同构的降维解释

如果有人告诉你，"证明一个定理"和"编写一个函数"是完全相同的事情，你会怎么想？

你大概会觉得这是某位数学教授在喝了第三杯浓缩咖啡后说的醉话。证明嘛，那是数学家的活儿——推导、归纳、反证法。编程嘛，那是程序员的活儿——数据结构、算法、API 调用。这两个世界有什么关系？

答案是：它们是同一个世界的两个面。而连接它们的那座桥，就是 Curry-Howard 同构。

这是本书的智力巅峰。但我向你保证，你不需要数学博士学位就能理解它。你只需要能读懂 Python 的 class 和 function。

从一个 Python 类开始

你在 Python 中定义一个类是什么意思？

class GreaterThanZero:
    def __init__(self, n: int, proof: str):
        assert n > 0, proof
        self.n = n

这个类叫 GreaterThanZero。它描述了一种东西——"大于零的整数"。类本身不是任何具体的整数。它是一个蓝图、一个规范、一种约束。

当你写 x = GreaterThanZero(5, "5 > 0") 时，你创建了一个实例。这个实例是对那个规范的一个具体实现——它是一个真实存在的、满足约束的对象。

现在，做一个思维替换。

如果"类的定义"不再是数据类型的蓝图，而是一个数学命题的陈述呢？如果"创建实例"不再是构造对象，而是给出一个证明呢？

在这种理解方式下：

命题 = 类型。证明 = 程序（构造该类型的对象）。

这就是 Curry-Howard 同构的核心要义。

在 Lean4 中看到真相

让我们把这个想法落地到 Lean4 的代码中。

在 Lean4 中，当你写下一个命题：

theorem my_theorem : 1 + 1 = 2 := by
  rfl

1 + 1 = 2 是一个类型。确切地说，它是 Eq Nat 2 2 这个类型的简写。而 rfl——你的老朋友——是构造这个类型的一个实例。

当你说"我证明了 1 + 1 = 2"，你在 Lean4 的内部世界中实际上做的事情是："我构造了一个类型为 1 + 1 = 2 的对象。"

证明存在等价于可以构造一个该类型的对象。命题为假等价于该类型没有任何可能的居民——你永远无法构造出一个满足条件的对象。

这不是一个比喻。不是一个启发式的类比。在 Lean4 的类型理论中，这就是字面上的实现方式。命题就是类型。证明就是值。

函数就是蕴含

让我们再深入一步。

在逻辑学中，蕴含是这样的："如果 P 成立，那么 Q 成立。"记作 P → Q。

在编程中，函数是这样的："给我一个类型为 P 的输入，我返回一个类型为 Q 的输出。"记作 P → Q。

注意到了吗？逻辑蕴含和函数签名用的是同一个符号——箭头。这不是巧合。

当你在 Lean4 中写一个从 P 到 Q 的函数时，你同时在证明一个蕴含命题："如果 P 成立，那么 Q 成立。"函数体就是证明过程——你把一个 P 类型的证据转化成了一个 Q 类型的证据。

-- 逻辑含义：如果 P 蕴含 Q，且 Q 蕴含 R，那么 P 蕴含 R
theorem imp_trans (hpq : P → Q) (hqr : Q → R) : P → R :=
  fun hp => hqr (hpq hp)

看这段代码。hpq 是一个"从 P 到 Q"的函数——也就是" P 蕴含 Q"的证明。hqr 是一个"从 Q 到 R"的函数。我们要证明 P 蕴含 R。怎么做？写一个从 P 到 R 的函数：接收一个 P 类型的值 hp，先用 hpq 把它变成 Q，再用 hqr 把它变成 R。

函数组合就是蕴含的传递性。你在写代码的同时完成了逻辑推导。

关于"逻辑与"和"逻辑或"

Curry-Howard 同构不只适用于蕴含。所有的逻辑连接词都有其类型论的对应物。

逻辑与（P ∧ Q）对应于一个二元组。要证明 P 且 Q，你得同时拿出 P 的证明和 Q 的证明，把它们打包成一对。

theorem and_intro (hp : P) (hq : Q) : P ∧ Q :=
  And.intro hp hq

逻辑或（P ∨ Q）对应于一个联合类型。要证明 P 或 Q，你只需要拿出其中一个的证明。

theorem or_left (hp : P) : P ∨ Q :=
  Or.inl hp

否定（¬P）对应于一个从 P 到矛盾（空类型 False）的函数。如果你能证明"假设 P 成立会导致矛盾"，那你就证明了 P 不成立。

-- ¬P 的定义就是 P → False

全称量词（∀）对应于依赖函数。存在量词（∃）对应于依赖对。

每一个逻辑概念都有一个编程概念的精确对应。反之亦然。

这对你意味着什么

如果你是一个有经验的程序员，Curry-Howard 同构给了你一个极其实用的思维工具。

当你面对一个需要证明的命题时，你不需要像一个数学家那样"灵光乍现"。你只需要像一个程序员那样思考："我需要构造一个满足这种类型签名的值。我手里有哪些原材料？我能通过什么函数组合来得到目标类型的值？"

证明就是编程。寻找证明就是寻找一种满足类型约束的构造方式。

Lean4 的编译器在做的事情——检查你的证明是否正确——本质上就是类型检查。它在验证你构造的值是否真的属于你声称的类型。

这就是为什么编译器能够做绝对裁决的法官。类型检查是机械的、确定性的、不可欺骗的。

实践：你的第一个"命题即类型"

让我们把理论落地。请在 Lean4 编辑器中输入以下代码：

-- 声明两个命题变量
variable (P Q : Prop)

-- 证明：如果 P 成立，那么 P 或 Q 成立
theorem p_implies_p_or_q : P → P ∨ Q := by
  intro hp
  exact Or.inl hp

拆解：intro hp 说的是"假设 P 成立，把这个假设叫做 hp"——你传唤了一个证人。exact Or.inl hp 说的是"P 或 Q 成立的证据就是 P 成立——左边那个就够了"——你提交了物证。

编译通过。法官认可。

你刚才做的事情，用 Curry-Howard 的语言来说，就是：你定义了一个从 P 到 P ∨ Q 的函数。输入是一个 P 类型的值，输出是一个 P ∨ Q 类型的值。证明和编程，一模一样。

在你内化这个同构之后，整个 Lean4 的世界将对你敞开。后面的每一个策略——intro、apply、exact、cases——都不再是神秘的咒语，而是你在"类型空间"中导航的工具。

接下来，我们将回到数据结构的领地。你已经见过了 Nat 的归纳定义。现在，让我们用同样的方式定义一棵二叉树——然后看看编译器如何强制你不遗漏任何一个分支。

参考资料

引用来源表

原始链接列表

https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html
https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf

第 6 章：拆解黑盒——代数数据类型与模式匹配

在 Python 中处理多种可能性的标准姿势长这样：

def describe(shape):
    if shape["type"] == "circle":
        return f"圆，半径 {shape['radius']}"
    elif shape["type"] == "rectangle":
        return f"矩形，宽 {shape['width']}，高 {shape['height']}"
    elif shape["type"] == "triangle":
        return f"三角形"
    else:
        return "未知形状"

这段代码有三个致命问题。

第一，如果有人给 shape["type"] 传了一个拼写错误——比如 "rectagle"——你不会得到编译错误。你会得到一个沉默的 "未知形状"。bug 被悄无声息地吞掉了。

第二，如果你以后新增了一种形状——比如 "pentagon"——编译器不会提醒你更新这个函数。你可能在三个月后的某次线上事故中才发现，五边形一直被归类为"未知形状"。

第三，else 分支是一个黑洞。它吞掉一切不匹配的输入，让你永远无法确认自己是否遗漏了什么情况。

Lean4 用归纳类型和模式匹配彻底解决了这三个问题。

用上帝视角定义一棵二叉树

在 Lean4 中，你不用字典和字符串标签来描述数据的种类。你用归纳定义——明确列举出数据的所有可能构造方式，一种不多、一种不少。

让我们定义一棵二叉树：

inductive Tree (α : Type) where
  | leaf : Tree α
  | node : Tree α → α → Tree α → Tree α

两行代码。没有第三种可能性。

这棵树要么是一片叶子 leaf（空树），要么是一个节点 node，包含左子树、一个值和右子树。这就是全部。编译器现在知道了这棵树的完整拓扑——没有隐藏选项、没有"else"后门、没有运行时的惊喜。

对比 Python 的写法：

class Tree:
    pass

class Leaf(Tree):
    pass

class Node(Tree):
    def __init__(self, left, value, right):
        self.left = left
        self.value = value
        self.right = right

Python 的版本看起来合理，但它没有闭合性。任何人随时可以再定义一个 class Stump(Tree): pass，然后你的所有 isinstance 检查都不会报错——它们只会进入 else 分支，悄无声息地产出错误结果。

归纳类型是封闭的。一旦定义完毕，数据的所有可能形态就被锁死了。编译器基于这个封闭性来做出它的裁决。

模式匹配：法官的穷举审查

定义了数据结构之后，你需要对它做操作。在 Lean4 中，这意味着模式匹配。

让我们计算一棵树中所有节点的数量：

def countNodes : Tree α → Nat
  | Tree.leaf => 0
  | Tree.node left _ right => 1 + countNodes left + countNodes right

每种构造方式对应一个分支。第一行处理 leaf（没有节点，返回 0）。第二行处理 node（当前节点算 1，加上左右子树的节点数）。

现在，试试故意漏掉一个分支：

def countNodes : Tree α → Nat
  | Tree.node left _ right => 1 + countNodes left + countNodes right
  -- 忘了处理 leaf

编译器不会让你过关。它会给你一条冷冰冰的错误信息："missing cases: Tree.leaf"。

在 Python 中遗漏一个分支，你需要等到运行时才能发现。在 Lean4 中，遗漏一个分支是一个编译错误。它不会等到你的代码在生产环境中跑了三个月之后、在一个罕见的边界条件下、在凌晨三点把你从床上叫起来。它会在你按下保存键的那一秒就告诉你。

这就是穷尽性检查的威力。编译器在说："我知道你的数据有哪些可能的形态。你必须对每一种形态都给出回应。不许偷懒。不许写 else。"

构建一个小型计算器

让我们用归纳类型和模式匹配做一个更有意思的东西——一个算术表达式的抽象语法树。

inductive Expr where
  | num : Int → Expr
  | add : Expr → Expr → Expr
  | mul : Expr → Expr → Expr

一个表达式要么是一个数字 num，要么是两个表达式的加法 add，要么是两个表达式的乘法 mul。

对这棵语法树做求值：

def eval : Expr → Int
  | Expr.num n => n
  | Expr.add a b => eval a + eval b
  | Expr.mul a b => eval a * eval b

三个分支。穷尽。没有遗漏。编译通过。

#eval eval (Expr.add (Expr.num 3) (Expr.mul (Expr.num 2) (Expr.num 5)))
-- 输出 13

如果你以后想新增一种运算——比如减法——你只需要在 Expr 的定义中加一行 | sub : Expr → Expr → Expr。编译器会立刻在所有使用了 Expr 的模式匹配处报红，强制你把新分支的处理逻辑补上。

这不是一个可选的代码质量工具。这是语言层面的强制约束。

"Python 3.10 也有模式匹配了"

你可能想起了 Python 3.10 引入的 match 语句。确实，语法上它看起来和 Lean4 的模式匹配相似。但本质区别在于：Python 的 match 不做穷尽性检查。

match shape:
    case Circle(r):
        print(f"半径 {r}")
    case Rectangle(w, h):
        print(f"宽 {w} 高 {h}")
    # 漏掉了 Triangle？没人会告诉你。

Python 不会报错。它只是不匹配。你的三角形会被无声地忽略。这种沉默的遗漏是 bug 的温床。

Lean4 的模式匹配和 Python 的 match 语句之间的差距，就像一个严格的法官和一个打了瞌睡的保安之间的差距。

实践：动手定义你的数据

打开 Lean4 编辑器。定义一个简单的交通灯类型和对它的模式匹配处理：

inductive TrafficLight where
  | red
  | yellow
  | green

def action : TrafficLight → String
  | TrafficLight.red => "停车"
  | TrafficLight.yellow => "减速"
  | TrafficLight.green => "通行"

编译它。然后故意删掉一个分支，看看编译器怎么说。

这种"删一个分支然后看报错"的练习，是内化穷尽性检查最快的方式。一旦你习惯了编译器替你兜底，你就再也回不去那个"else 吞掉一切"的世界了。

接下来，我们将面对纯函数式编程最大的哲学困境：如果世界是不可变的，那么怎么向控制台打印一行字？答案藏在一个叫 IO Monad 的防爆箱里。

参考资料

引用来源表

原始链接列表

https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html
https://lean-lang.org/functional_programming_in_lean/getting-to-know/datatypes-and-patterns.html
https://peps.python.org/pep-0634/

第 7 章：与现实世界的肮脏接口——IO Monad

你已经在一个纯粹的数学世界里待了三章。在那个世界里，没有副作用、没有可变状态、没有文件读写、没有网络请求。一切都是透明的、确定的、可证明的。

但现在你面对一个尴尬的现实：你连一行字都打印不出来。

一个不能与外部世界交互的程序，就像一个密封在真空中的引擎——理论上完美，实践上无用。你最终需要读取用户输入、写入文件、发送 HTTP 请求。这些操作本质上是不纯的：每次读取用户输入的结果都不一样，写文件会改变磁盘状态，网络请求可能成功也可能超时。

纯函数不允许这些事情发生。那怎么办？

答案不是放弃纯粹性。答案是建造一个防爆箱。

防爆箱模型

想象你在一个无尘实验室里工作。实验室里的一切都必须保持绝对洁净——这是你的纯粹函数的世界。但你偶尔需要从外面拿进来一些原材料（用户输入），或者把成品送出去（屏幕输出）。

你不会把实验室的门打开，让外面的灰尘涌进来。你会使用一个传递仓——一个密封的中转装置。你把需要的东西放进传递仓，关上外面的门，打开里面的门，取出东西。实验室始终保持洁净。

在 Lean4 中，IO Monad 就是这个传递仓。

当你写下一个类型为 IO String 的表达式时，你并没有在执行一个副作用。你是在描述一个"将会产生副作用的计划"。这个计划被封装在 IO 类型的容器里，与你的纯粹逻辑世界完全隔离。

只有当整个程序作为可执行文件运行时，Lean4 的运行时才会打开这个容器、执行里面的计划。在编译阶段和证明阶段，这些副作用永远不会泄漏。

你好，世界

让我们写一个最简单的带副作用的程序：

def main : IO Unit := do
  IO.println "Hello, World!"

IO Unit 是这个函数的返回类型。IO 说明它包含副作用——具体地说，它会影响外部世界（打印到控制台）。Unit 说明它不返回任何有意义的值——就像 Python 函数返回 None。

do 关键词开启一个"副作用序列"——在 do 块里，你可以按顺序执行多个 IO 操作。IO.println 是一个向控制台打印一行文字的函数。

编译并运行这段代码：

$ lean --run Main.lean
Hello, World!

恭喜。你的 Lean4 程序终于和外部世界说话了。

读取用户输入

让我们做一个能交互的程序：

def main : IO Unit := do
  IO.print "请输入你的名字："
  let name ← IO.getStdin >>= fun stdin => stdin.getLine
  IO.println s!"你好，{name.trim}！欢迎来到法庭。"

注意那个 ← 符号。它是 do 块中的特殊语法，意思是"从 IO 容器中取出值"。IO.getStdin 返回的不是一行文字——它返回的是一个"读取标准输入的计划"。← 执行这个计划，把结果绑定到 name 变量上。

在 do 块之外，name 只是一个 IO String 类型的值——一个还没被执行的计划。在 do 块之内，← 让你可以"拆开"这个计划、拿到真正的 String。

这就是 IO Monad 的精妙之处：它不是禁止你做有副作用的事情，而是强制你在一个受控的环境中做这些事情，并且清楚地标记哪些代码是纯的、哪些是不纯的。

Lean4 不是学术玩具

到目前为止，你可能仍然觉得 Lean4 主要是一个用来证明数学定理的工具。让我打破这个印象。

Lean4 的编译器可以把你的代码编译成 C 语言，然后进一步编译成原生的可执行文件。这不是通过某个实验性的后端实现的——这是 Lean4 的核心设计。Lean4 本身的编译器就是用 Lean4 编写的（自举），然后编译成 C 来运行。

这意味着你用 Lean4 写的程序不仅仅是"可以运行"——它们可以高效地运行。引用计数替代垃圾回收、尾递归优化、内存布局控制——这些都是 Lean4 在工程层面的实打实的能力。

所以当有人对你说"Lean4 只是一个学术项目"时，你可以告诉他：Lean4 的编译器比大多数 Python 项目都更接近底层硬件。

实战：命令行计算器

融合前面学到的归纳类型、模式匹配和 IO，让我们写一个简单的命令行计算器：

def calculate (input : String) : String :=
  match input.trim.splitOn " " with
  | [a, "+", b] =>
    match (a.toInt?, b.toInt?) with
    | (some x, some y) => s!"结果：{x + y}"
    | _ => "错误：无效的数字"
  | [a, "*", b] =>
    match (a.toInt?, b.toInt?) with
    | (some x, some y) => s!"结果：{x * y}"
    | _ => "错误：无效的数字"
  | _ => "错误：请输入格式如 '3 + 5' 的表达式"

def main : IO Unit := do
  IO.println "欢迎使用 Lean4 命令行计算器"
  IO.print "> "
  let input ← (← IO.getStdin).getLine
  IO.println (calculate input)

注意 calculate 函数本身是一个纯函数——它接收一个 String，返回一个 String，没有任何副作用。所有的 IO 操作都被隔离在 main 函数中。

这就是 IO Monad 的最佳实践：把尽可能多的逻辑写成纯函数，把 IO 压缩到最薄的一层。纯函数可以被测试、被证明、被推理。IO 层只负责搬运数据。

关于 Monad 的那个词

你可能已经注意到我一直在用"IO Monad"这个词，但从未正式定义过"Monad"是什么。这是有意的。

在函数式编程社区里，Monad 是一个被过度神秘化的概念。有人用范畴论解释它，有人用墨西哥卷饼解释它，有人用宇航服解释它。这些解释大多让初学者更加困惑。

对于本书而言，你只需要知道这些：Monad 是一种设计模式，它让你能在纯函数式语言中按顺序组合带有"效果"的操作。IO 是一种特定的 Monad，它的"效果"是与外部世界交互。do 块是使用 Monad 的语法糖。← 是从 Monad 中提取值的操作。

你不需要理解 Monad 的范畴论定义，就像你不需要理解 CPU 的晶体管结构就能写 Python 程序一样。如果你将来对底层理论产生了兴趣，Lean4 社区有大量的深入资料。但在那之前，把 IO 当成一个"副作用防爆箱"就完全足够了。

你已经走过了第二篇的全部旅程。你杀死了可变状态，看见了命题与类型的同构，拆解了归纳类型的黑盒，学会了用 IO 防爆箱与现实世界握手。

是时候回到法庭了。

在第三篇中，我们将正式开始策略训练——不再是简单的 rfl，而是完整的审问技巧体系。第一课：如何传唤证人、如何适用先例、如何做出结案陈词。

参考资料

引用来源表

原始链接列表

https://lean-lang.org/functional_programming_in_lean/hello-world.html
https://github.com/leanprover/lean4
https://leanprover.github.io/lean4/doc/

第 8 章：剥洋葱的艺术——命题逻辑的审问技巧

法庭进入正式审理程序。

在前面的章节中，你已经认识了 Infoview 面板、学会了用 rfl 处理最简单的等式证明。但 rfl 只能在等号两边化简后完全相同时才起作用。面对真正的命题逻辑——蕴含、合取、析取、否定——你需要一套更完整的审问技术。

想象你面前摆着一个五层嵌套的命题。它的结构像一颗洋葱——外面包着"如果...那么..."，里面裹着"...且..."，最核心处藏着一个你需要证明的结论。你的任务是一层一层剥开它，直到核心暴露无遗。

本章教你三种基础审问技巧。它们是你在法庭上最常用的三把武器。

第一式：intro——传唤证人

当你面对一个形如 P → Q 的命题时——"如果 P 成立，那么 Q 成立"——你的第一步是什么？

假设 P 成立。

这就是 intro 的作用。它说："好，我假设 P 成立。让我把这个假设叫做 hp，放到我的证据库里。现在我只需要证明 Q 就行了。"

example (P Q : Prop) (hpq : P → Q) (hp : P) : Q := by
  apply hpq
  exact hp

等等，这里我们一下用了两个策略。让我慢慢拆解。

先看一个更纯粹的 intro 例子：

example : P → P := by
  intro hp
  exact hp

Infoview 的变化过程是这样的：

开始时，Goal 是 P → P。你需要证明"如果 P 成立，那么 P 成立"。你执行 intro hp——传唤证人。现在 Context 中多了一条假设 hp : P（P 成立的证据），Goal 变成了 P。你只需要证明 P——而 hp 就是 P 的证据。执行 exact hp——结案陈词，直接把 hp 提交给法官。

Goal 消失。证明完成。

intro 的本质是：把一个蕴含命题的前提"引入"到你的假设库中，从而简化你需要证明的目标。每次你看到 Goal 里有一个箭头 →，你的第一反应应该是 intro。

第二式：apply——适用先例

法庭上经常有这种情况：你需要证明结论 Q，但你手里没有 Q 的直接证据。不过你知道一条规则——如果 P 成立，那么 Q 就成立。而你碰巧有 P 的证据。

这时候你需要 apply——向法官申请适用一条已有的规则或先例。

example (P Q : Prop) (hpq : P → Q) (hp : P) : Q := by
  apply hpq
  exact hp

开始时，Goal 是 Q。你的 Context 中有 hpq : P → Q 和 hp : P。

你执行 apply hpq。这相当于对法官说："我要用 hpq 这条先例。它说如果 P 成立则 Q 成立。所以如果我能证明 P，Q 就自动成立。" 法官接受了。Goal 从 Q 变成了 P。

然后 exact hp——你手里正好有 P 的证据。提交。结案。

apply 的威力在于它让你反向推理。你不是从假设出发一步步推到结论，而是从结论出发说"要证明这个结论，我只需要证明那个前提"。这是一种极其高效的推理方式——先确定目标需要什么，再去寻找原材料。

第三式：exact——结案陈词

exact 是最简单也最终极的策略。当你的 Context 中已经有了一个和 Goal 完全匹配的证据时，你直接把它拍在法官桌上。

example (P : Prop) (hp : P) : P := by
  exact hp

没有推理过程。没有中间步骤。就是："法官大人，这就是证据。一模一样。请结案。"

exact 要求你提供的东西在类型上与 Goal 完全一致。不多不少。这是最精确的一击。

三把武器的组合

让我们来一道稍微复杂的题，体验三把武器如何配合：

example (P Q R : Prop) (hpq : P → Q) (hqr : Q → R) : P → R := by
  intro hp
  apply hqr
  apply hpq
  exact hp

用法庭语言翻译：

法庭需要证明"如果 P 成立，那么 R 成立"。

第一步，intro hp：传唤证人。假设 P 成立，叫它 hp。目标变成证明 R。

第二步，apply hqr：适用先例。hqr 说了，Q 蕴含 R。所以如果我能证明 Q，R 自然成立。目标变成证明 Q。

第三步，apply hpq：再适用先例。hpq 说了，P 蕴含 Q。所以如果我能证明 P，Q 自然成立。目标变成证明 P。

第四步，exact hp：结案陈词。hp 就是 P 的证据。正好。

四步。干净利落。每一步都有据可查，每一步都被编译器实时验证。

让 AI 画逻辑依赖树

面对更复杂的命题时，你可能会迷失方向——不知道应该先 intro 还是先 apply，不确定该用哪条先例。

这正是 AI 辩护律师的用武之地。

尝试给 AI 这样的 Prompt："我需要证明以下 Lean4 命题：[贴命题]。请不要直接写证明。请先画出这个命题的逻辑依赖树——哪些假设可以推出哪些中间结论，最终如何推出目标。"

AI 生成的逻辑依赖树可能不完全正确，但它能帮你看清命题的整体结构——就像在迷宫入口处先看一眼地图。然后你再用 intro、apply、exact 这三把武器，一步步在编辑器中执行审问。每一步都有编译器的即时反馈。

AI 负责战略视野。你负责战术执行。编译器负责最终裁决。

实践：五道命题逻辑热身

试着独立完成以下五道练习。如果卡住了，回头看看三种策略的用法，或者启用红绿灯闭环让 AI 辅助你。

-- 1. 恒等蕴含
example (P : Prop) : P → P := by
  sorry

-- 2. 蕴含的传递性
example (P Q R : Prop) : (P → Q) → (Q → R) → P → R := by
  sorry

-- 3. 合取消去（拆开 And）
example (P Q : Prop) : P ∧ Q → P := by
  sorry

-- 4. 合取引入（构建 And）
example (P Q : Prop) : P → Q → P ∧ Q := by
  sorry

-- 5. 析取引入（构建 Or）
example (P Q : Prop) : P → P ∨ Q := by
  sorry

sorry 是 Lean4 中的"占位符"——它告诉编译器"这里的证明我还没写"。编译器会发出警告但不会报错。你的任务是把每个 sorry 替换为真正的证明。

当你完成全部五道题、编辑器中看不到任何黄色警告时，你就从命题逻辑的新手毕业了。

下一章，我们将面对一个新的逻辑层次。在命题逻辑中，我们处理的是固定的命题——P 成立或不成立。但在谓词逻辑中，命题开始涉及"任意"和"存在"——我们需要处理量词的幽灵。

参考资料

引用来源表

原始链接列表

https://leanprover.github.io/theorem_proving_in_lean4/tactics.html
https://leanprover.github.io/theorem_proving_in_lean4/propositions_and_proofs.html

第 9 章：存在与虚无——捕获量词的幽灵

在上一章中，你处理的所有命题都是固定的：P 成立或不成立，Q 蕴含 R 或不蕴含。命题逻辑的世界像一盘已经摆好的棋——棋子的位置是确定的，你要做的只是找到一条通往胜利的路径。

但谓词逻辑打开了一个全新的维度。

命题不再是固定的"P"和"Q"。它们开始涉及变量——"对于所有 x"、"存在某个 y"。你不再是在已知的棋盘上移动棋子，而是在一个无限延伸的空间中追捕幽灵。

这两种量词——全称量词（∀）和存在量词（∃）——是证明的两大基本姿态。它们要求的策略截然不同，就像控方说"所有嫌疑人都有不在场证明"和"存在一个嫌疑人没有不在场证明"时，审理的方向完全不同。

全称量词：应对"任意"的挑战

当你需要证明"对于所有自然数 n，某个性质 P(n) 成立"时，你面临一个不可能逐一验证的困境——自然数有无穷多个。

策略是：引入一个任意的 n。

如果你能证明对于一个完全未指定的 n，P(n) 仍然成立，那么它必定对所有 n 都成立——因为你没有利用 n 的任何特殊性质。

在 Lean4 中，这仍然用 intro 策略完成：

example : ∀ (n : Nat), 0 + n = n := by
  intro n
  simp

intro n 把"对于所有 n"变成了"给定一个任意的 n，证明 0 + n = n"。量词消失了，你只需要对这个具体（但未指定）的 n 完成证明。这里我们偷跑了一个新策略 simp（simplify 的缩写），它能自动化简很多基础等式——我们在第12章会详细讨论它。

全称量词的证明模式总结：看到 ∀，用 intro 传唤一个"任意的证人"。然后针对这个证人完成证明。

存在量词：提交物证

存在量词的证明逻辑恰好相反。

当你需要证明"存在某个 n 使得某个性质成立"时，你不需要证明所有 n 都满足——你只需要找到一个具体的 n，然后证明它确实满足条件。

在 Lean4 中，提交存在性证据使用 use 策略：

example : ∃ (n : Nat), n + n = 4 := by
  use 2

你对法官说："存在这样一个自然数。具体来说，它是 2。" 然后编译器自动验证 2 + 2 = 4 确实成立。案件关闭。

use 就像在法庭上提交物证——你拿出一个具体的对象，声称它满足条件，法官当场核实。

拆包存在性证据：rcases

有时候你不是要证明一个存在命题，而是要使用一个已知的存在命题作为推理的素材。

假设你知道"存在一个 n 使得 P(n) 成立"，现在你想用这个事实来推导其他结论。你需要把这个存在性声明"拆开"，拿到里面那个具体的 n 和 P(n) 的证据。

这就是 rcases 的作用——它是一个强大的分解工具，能拆开各种复杂的结构。

example (h : ∃ (n : Nat), n > 5) : ∃ (m : Nat), m > 3 := by
  rcases h with ⟨n, hn⟩
  use n
  linarith

rcases h with ⟨n, hn⟩ 的意思是："我知道存在一个 n 满足某些条件。让我把这个 n 取出来叫它 n，把'n > 5'的证据取出来叫它 hn。" 现在你的 Context 中有了具体的 n : Nat 和 hn : n > 5。

然后 use n 提交了一个物证——就用刚拆出来的那个 n——声称它大于 3。最后 linarith（线性算术自动化求解器）替你搞定了"n > 5 蕴含 n > 3"这个显而易见的推理。

"数学符号看不懂"

如果你看到 ∀ 和 ∃ 就心里打鼓，让我翻译一下：

∀ (x : T), P(x) 就是：给我任何一个 T 类型的 x，P(x) 都成立。用 Python 的话说，相当于：

assert all(P(x) for x in all_possible_T_values)

∃ (x : T), P(x) 就是：存在至少一个 T 类型的 x，使得 P(x) 成立。用 Python 的话说：

assert any(P(x) for x in all_possible_T_values)

区别在于：Python 的 all 和 any 只能对有限集合做运行时检查。Lean4 的 ∀ 和 ∃ 是编译时的数学证明——它们覆盖所有可能的值，包括无限集合。

组合实战：嵌套量词

真正的证明很少只涉及一个量词。让我们看一道涉及嵌套量词和逻辑连接词的题目：

example : (∀ x : Nat, x = x) := by
  intro x
  rfl

简单热身。每个自然数都等于自身——intro 引入一个任意的 x，rfl 搞定自反性。

来一道稍微有分量的：

example : ∀ (n : Nat), ∃ (m : Nat), m = n + 1 := by
  intro n
  use n + 1

对于任意自然数 n，存在一个自然数 m 使得 m = n + 1。策略：引入任意 n，然后提交 n + 1 作为 m 的物证。编译器自动验证 n + 1 = n + 1。

最后来一道把 rcases、use 和逻辑连接词组合在一起的：

example (h : ∃ n : Nat, n > 0 ∧ n < 10) : ∃ m : Nat, m < 10 := by
  rcases h with ⟨n, _, hn_lt⟩
  use n
  exact hn_lt

已知条件说：存在一个大于 0 且小于 10 的自然数。结论说：存在一个小于 10 的自然数。拆开已知条件，取出 n 和它小于 10 的证据（用 _ 忽略大于 0 的证据，因为我们不需要它），然后用这个 n 作为物证提交。

实践：证明"存在一个偶数大于 2"

尝试独立完成这道练习。你可以定义一个简单的偶数判定（或者用 Lean4 的算术能力直接构造）：

example : ∃ (n : Nat), n > 2 ∧ n % 2 = 0 := by
  use 4
  sorry -- 替换为你的证明

提示：use 4 提交了你的物证。然后你需要证明 4 > 2 ∧ 4 % 2 = 0。拆成两部分分别证明——提示：constructor 策略可以把 ∧ 目标拆成两个子目标。

在你习惯了量词的操作模式之后，下一章我们将面对一个终极挑战——证明一条真正的数学定律。一个2000多年前亚里士多德就知道的定律，但你要让编译器亲自确认它。

参考资料

引用来源表

原始链接列表

https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/RCases.html
https://leanprover.github.io/theorem_proving_in_lean4/tactics.html

第 10 章：密室逃脱——用 AI 重构集合论直觉

你上一次想到集合论是什么时候？

大概是高中数学课本上的维恩图。两个椭圆交叉在一起，阴影部分代表交集，整个圆圈合在一起代表并集。老师在黑板上画完图，让你数阴影区域的元素个数。

那种理解方式——把集合当成一堆东西装在一个圈里——在直觉层面没有问题。但在 Lean4 的世界里，集合的底层实现和维恩图完全不是一回事。

集合不是容器。集合是函数。

集合就是谓词

在 Lean4（以及大多数形式化数学系统）中，一个集合 S 本质上是一个谓词函数——一个从元素到命题的映射。"x 属于集合 S" 等价于 "谓词 S(x) 成立"。

-- 一个集合就是一个判断函数
-- Set α 的底层定义本质上是 α → Prop

所谓"偶数集合"，不是一个装着 0, 2, 4, 6... 的盒子。它是一个函数：给它一个自然数 n，它返回命题 "n % 2 = 0"。如果这个命题为真，n 就"属于"这个集合。如果为假，n 就"不属于"。

这种视角一旦建立，集合的交并补操作就变成了纯粹的逻辑运算：

交集 A ∩ B 就是"A(x) 且 B(x)"——两个谓词同时成立。

并集 A ∪ B 就是"A(x) 或 B(x)"——至少一个谓词成立。

补集 Aᶜ 就是"非 A(x)"——谓词不成立。

维恩图只是这些逻辑运算的可视化。底层全是你在第八、九章学过的命题逻辑和谓词逻辑。

德·摩根定律：大案要案

现在让我们来做一个真正的证明项目。

德·摩根定律说的是：一个并集的补等于两个补集的交。用数学符号写：(A ∪ B)ᶜ = Aᶜ ∩ Bᶜ。

用自然语言翻译：如果一个元素不属于 A 也不属于 B，那等价于说它既不属于 A 又不属于 B。

听起来很直觉。但在 Lean4 中严格证明它，你需要把这个"直觉"拆解成五个精确的逻辑步骤。

这是 Vibe Coding 的绝佳练习场。让我们看看如何指导 AI 拆解这个证明。

证明策略：拆成子引理

给 AI 的 Prompt 可以是这样的：

"在 Lean4 中，我需要证明德·摩根定律：对于任意集合 A 和 B，(A ∪ B)ᶜ = Aᶜ ∩ Bᶜ。请将这个证明拆解为多个子步骤（Lemmas），每个步骤只用到基础的谓词逻辑策略。"

一个合理的拆解方式是证明两个方向的子集关系——"左边是右边的子集"和"右边是左边的子集"——然后由双向子集关系得出等式。

对于每个方向，证明的核心步骤是：

第一步，取一个任意元素 x。

第二步，假设 x 属于左边的集合。

第三步，证明 x 属于右边的集合。

展开集合的定义后，这些步骤会变成纯粹的命题逻辑推导——恰好是你在前两章练过的技术。

核心证明片段

以下是其中一个方向的证明——(A ∪ B)ᶜ ⊆ Aᶜ ∩ Bᶜ：

example (A B : Set α) : (A ∪ B)ᶜ ⊆ Aᶜ ∩ Bᶜ := by
  intro x hx
  constructor
  · intro ha
    apply hx
    left
    exact ha
  · intro hb
    apply hx
    right
    exact hb

一步步来：

intro x hx：取任意元素 x，假设 x 属于 (A ∪ B)ᶜ。也就是说，x 不属于 A ∪ B。hx 的类型是 x ∉ A ∪ B，展开后就是 ¬(x ∈ A ∨ x ∈ B)。

constructor：把目标 Aᶜ ∩ Bᶜ 拆成两个子目标——证明 x ∈ Aᶜ 和 x ∈ Bᶜ。

对于第一个子目标 x ∈ Aᶜ（即 x ∉ A）：假设 x ∈ A（intro ha），然后通过 apply hx 和 left; exact ha 推出矛盾——因为如果 x ∈ A，那么 x ∈ A ∪ B，与 hx 矛盾。

对于第二个子目标 x ∈ Bᶜ：同理。

每一步都在 Infoview 面板中有即时反馈。你可以看到 Context 如何增长、Goal 如何缩小、子目标如何被逐个消灭。

从碎片到完整

另一个方向的证明——Aᶜ ∩ Bᶜ ⊆ (A ∪ B)ᶜ——留给你作为练习。提示：这次你需要使用 rcases 来拆开"A ∪ B"的析取结构，然后分别利用"不属于 A"和"不属于 B"的假设来达到矛盾。

两个方向的子集关系证完后，德·摩根定律就得证了。

这个过程展示了 Lean4 证明的一个核心模式：宏大的定理被拆解为琐碎但可验证的子引理。每一块子引理都小到可以用几行策略搞定、小到编译器可以逐步验证。AI 帮你找到拆解的方向，你用策略执行每一步，编译器在每一步上盖章确认。

没有任何步骤是凭直觉跳过的。没有任何推理是"看起来对"就通过了的。

"证明数学定理对写软件有什么用？"

也许你心里正在产生这个疑问。

答案在第十五章——但我现在可以给你一个预告：当你证明了"对于所有列表，插入排序的输出一定是有序的且是原列表的排列"时，你用到的策略和证明结构，与你刚才证明德·摩根定律用到的完全一样。

集合论的证明训练不是为了让你成为数学家。它是在训练你的一种思维肌肉——把模糊的直觉分解为精确的逻辑步骤，然后让机器验证每一步。这种肌肉在证明排序算法的正确性时，和在证明集合定律时，是同一块肌肉。

你正在为最终的加冕时刻做准备。

接下来，我们将离开命题逻辑的领地，进入数学的纵深——自然数的归纳法。如果说策略是你的横向技能，那么归纳法就是你的纵向引擎，让你能够驯服无限。

参考资料

引用来源表

原始链接列表

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html
https://leanprover-community.github.io/mathematics_in_lean/
https://leanprover.github.io/theorem_proving_in_lean4/quantifiers_and_equality.html

第 11 章：驯服无限——皮亚诺公理与归纳法引擎

如果你连"1 + 1 = 2"都不能在编译器中证明，你凭什么相信你的排序算法？

这不是修辞性反问。在 Lean4 中，自然数不是从天而降的原始概念。每一条关于自然数的性质——包括最基础的加法等式——都需要从零开始被证明。而驯服自然数的唯一合法工具，就是归纳法。

你在高中学过数学归纳法。老师说：先证基础情况（n = 0），再假设 n = k 时成立并证明 n = k+1 时也成立。然后所有自然数的情况就都搞定了。

当时你可能做题很熟练但从未真正理解它为什么有效。现在，让 Lean4 的编译器帮你把这个理解砸实。

数字的本质

回忆第四章。自然数在 Lean4 中是这样定义的：

inductive Nat where
  | zero : Nat
  | succ : Nat → Nat

零是自然数。任何自然数的后继也是自然数。除此之外没有自然数。

这意味着每个自然数都可以被"剥洋葱"——不断取前驱——直到剥到 zero。3 就是 succ (succ (succ zero))。编译器完全知道这棵结构长什么样。

归纳法的有效性正是建立在这种结构之上的。因为每个自然数都是从 zero 经过有限次 succ 构造出来的，所以如果你能证明某个性质对 zero 成立，且能证明它从 n 传递到 succ n，那么它对所有自然数都成立——因为没有其他来源的自然数。

你的第一个归纳证明

让我们证明：对于所有自然数 n，0 + n = n。

这看起来像废话。但在 Lean4 中，加法是这样递归定义的：

-- 加法的递归定义（简化版）
-- add m zero     = m
-- add m (succ n) = succ (add m n)

注意：加法是对第二个参数做递归。所以 add 0 n 并不会被自动化简——因为 n 不是一个具体的数，编译器不知道该走哪个分支。rfl 在这里无能为力。

你需要归纳法。

theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    simp [Nat.add_succ]
    exact ih

拆解一下：

induction n with 启动归纳法引擎。它将证明拆成两个子目标——基础情况和归纳步骤。

基础情况 | zero =>：证明 0 + 0 = 0。根据加法定义的第一条规则，add m zero = m，所以 0 + 0 = 0。rfl 搞定。

归纳步骤 | succ n ih =>：这里的 ih 是归纳假设——"假设 0 + n = n 已经成立"。你需要证明 0 + succ n = succ n。根据加法定义的第二条规则，0 + succ n = succ (0 + n)。用归纳假设 ih 把 0 + n 替换为 n，得到 succ n = succ n。rfl。

编译通过。你刚才用数学归纳法证明了一条关于所有自然数的性质。不是用测试验证了 100 个例子——而是数学证明了无穷多个。

当证明失败：发现缺失的引理

在实际操作中，你的第一次归纳证明尝试几乎一定会失败。不是因为你的逻辑错误，而是因为你会发现自己在某个步骤缺少一条基础引理。

比如你想证明加法交换律 n + m = m + n。你对 n 做归纳，在归纳步骤中需要用到 m + succ n = succ (m + n)——但这条引理你还没证明过。

这时候编译器的报错就成了你最好的向导。它冷冰冰地告诉你："我找不到 Nat.succ_add 这个引理。"于是你知道需要先证明这条辅助引理，再回来继续主证明。

这个"发现缺失引理 → 先证引理 → 回到主线"的过程，就是形式化证明的日常。你不是在做一道线性的题目——你在建造一座由引理构成的大厦，每一块砖都必须先烧好、先验证，才能砌上去。

实战：证明 0 + n = n 的完整过程

如果你卡住了，这里是一个完整的、可以通过编译的版本：

theorem zero_add' : ∀ n : Nat, 0 + n = n := by
  intro n
  induction n with
  | zero => rfl
  | succ n ih =>
    rw [Nat.add_succ]
    rw [ih]

这里用了一个新策略 rw——rewrite（重写）。rw [Nat.add_succ] 告诉编译器："在 Goal 中，把 0 + succ n 替换成 succ (0 + n)，根据 Nat.add_succ 这条已知引理。" 替换后 Goal 变成 succ (0 + n) = succ n。然后 rw [ih] 用归纳假设把 0 + n 替换成 n。Goal 变成 succ n = succ n。自动完成。

rw 是一把外科手术刀——它让你在等式中做精确的局部替换。我们在下一章将深入探讨它。

归纳法不只是自然数

最后让我指出一点：归纳法不限于自然数。任何归纳定义的类型——列表、二叉树、你在第六章定义的算术表达式——都可以用 induction 策略进行结构归纳。

对列表做归纳：基础情况是空列表 []，归纳步骤是"假设对列表 tail 成立，证明对 head :: tail 也成立"。

对二叉树做归纳：基础情况是 leaf，归纳步骤是"假设对左右子树都成立，证明对 node left val right 也成立"。

归纳法是你在 Lean4 中处理递归数据结构的万能钥匙。任何用 inductive 定义的类型，都天然携带着归纳原理。你不需要额外声明或配置——编译器自动提供。

接下来，我们将把 rw（重写）这把外科手术刀磨得更锋利，然后见识 ring 和 linarith 这两颗自动化核弹的暴力美学。

参考资料

引用来源表

原始链接列表

https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html
https://leanprover.github.io/theorem_proving_in_lean4/tactics.html
https://leanprover-community.github.io/mathematics_in_lean/

第 12 章：暴力与优雅——外科手术与核打击

到目前为止，你的每一次证明都是手工完成的。你用 intro 传唤证人、用 apply 适用先例、用 exact 结案、用 rw 做精确替换、用 induction 驯服自然数。每一步都由你亲手操控，每一步都清晰可追溯。

这很好。你需要经历这个阶段来理解证明的本质。

但现在，让我给你看一些会改变你对"证明"的感性认知的东西。

rw：外科手术刀

rw（rewrite）你在上一章已经见过了。让我们正式解析它的威力。

rw 的作用是在 Goal 或 Context 中做精确的等式替换。给它一条等式 h : a = b，它会在 Goal 中把所有的 a 替换成 b。

example (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by
  rw [h1]
  -- Goal 变成了 b = c
  rw [h2]
  -- Goal 变成了 c = c，自动完成

两步替换。第一步把 a 换成 b，第二步把 b 换成 c。最后编译器看到 c = c，自动收工。

rw 的方向可以反转——rw [← h1] 会把 b 替换回 a。你还可以指定替换的位置——只替换目标中的某个特定出现。

这是一把精确的外科手术刀。你知道要切哪里，你知道切完后会变成什么样。

simp：智能清洁工

simp（simplify）比 rw 更自动化。它会尝试用一组预定义的化简规则来简化 Goal，重复应用直到无法再简化。

example (n : Nat) : n + 0 = n := by
  simp

一个词。证明完成。simp 知道 Nat.add_zero 这条引理（"任何数加零等于自身"），自动应用了它。

你可以给 simp 额外的引理：

example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
  simp [h]

simp [h] 在化简时额外考虑了 h : a = b，把 a 替换为 b，然后化简得到 b + 1 = b + 1。

simp 是一个可靠的清洁工——它不会做错误的简化，但有时候它会因为找不到合适的规则而卡住。遇到这种情况，你需要手动补充 rw 来引导方向。

ring：代数核弹

现在进入重头戏。

ring 是一个自动化策略，专门处理交换环（commutative ring）上的代数等式。它能自动展开多项式、合并同类项、重新排列因子顺序，证明任何纯代数恒等式。

看这个例子：

example (a b : Int) : (a + b) * (a + b) = a * a + 2 * a * b + b * b := by
  ring

一个词。完美平方公式。证明完成。

手工证明这个等式需要多少步？你需要展开两次分配律、合并四项乘积、利用乘法交换律把 b * a 变成 a * b、然后把两个 a * b 合并成 2 * a * b。大约十几步 rw。

ring 一步搞定。

再来一个：

example (x y z : Int) : (x - y) * (x + y) = x^2 - y^2 := by
  ring

平方差公式。一步。

example (a b c : Int) : (a + b + c)^2 = a^2 + b^2 + c^2 + 2*a*b + 2*a*c + 2*b*c := by
  ring

三项展开。一步。

你开始感受到那种暴力美学了吗？

linarith：不等式终结者

如果 ring 是代数领域的核弹，那么 linarith（linear arithmetic）就是不等式领域的终结者。

linarith 能自动求解所有可以通过线性组合现有假设来证明的不等式。

example (a b : Int) (h1 : a > 0) (h2 : b > 0) : a + b > 0 := by
  linarith

一步。两个正数的和是正数。

example (x : Int) (h1 : x > 3) (h2 : x < 10) : x > 1 := by
  linarith

一步。如果 x 大于 3，那 x 当然大于 1。

example (a b c : Int) (h1 : a ≤ b) (h2 : b < c) : a < c := by
  linarith

一步。不等式的传递性。

linarith 的原理是在你的 Context 中找到涉及相关变量的所有不等式和等式，然后通过线性组合尝试推导出目标不等式。如果能推出来就通过，推不出来就报错。

对比：手术刀 vs 核弹

让我们用同一个命题展示两种证明风格。

证明：对于所有自然数 n，(n + 1) * (n + 1) = n * n + 2 * n + 1。

手工证明（外科手术风格）：

-- 手工版本（伪代码，展示步骤数量）
-- rw [Nat.mul_add]
-- rw [Nat.add_mul]
-- rw [Nat.add_mul]
-- rw [Nat.mul_one]
-- rw [Nat.one_mul]
-- rw [Nat.add_assoc]
-- rw [Nat.add_assoc]
-- ... 可能还有更多步

自动化证明（核打击风格）：

example (n : Nat) : (n + 1) * (n + 1) = n * n + 2 * n + 1 := by
  ring

一步。

手工版本是一座十几层高的代码山。自动版本是一行话。两者的正确性都被编译器完全验证。

何时用手术刀，何时用核弹

自动化策略不是万能的。ring 只处理代数等式——如果你需要利用某个特定的假设（比如 h : a = 3），你可能需要先用 rw [h] 把 a 替换掉，然后再用 ring。

linarith 只处理线性不等式——如果涉及乘法或幂运算的不等式（比如 a^2 ≥ 0），它可能无能为力。你需要用 nlinarith（nonlinear arithmetic）或先用其他策略化简。

simp 的威力取决于它的化简规则库——如果你用到了自定义的定义或引理，你需要手动添加。

经验法则是：先试 ring / linarith / simp。如果搞不定，退回到 rw 做精确的局部手术，然后再试自动化。

这种"先暴力尝试、不行再精修"的策略，和第二章的红绿灯闭环有异曲同工之处。让机器先试。失败了再由人类介入指导。

实践：亲身感受暴力美学

试几道题，体验一下从手工到自动化的爽感落差：

-- 1. 用 ring 证明
example (a b : Int) : (a + b)^3 = a^3 + 3*a^2*b + 3*a*b^2 + b^3 := by
  ring

-- 2. 用 linarith 证明
example (x y : Int) (h1 : x ≥ 0) (h2 : y ≥ 0) : x + y ≥ 0 := by
  linarith

-- 3. 组合使用
example (a : Int) (h : a > 5) : 2 * a > 10 := by
  linarith

一词定乾坤的快感。这就是自动化策略的暴力美学。

在下一章，我们将进入一个巨人的军火库——Mathlib，人类历史上最庞大的形式化数学代码库。在那里，你会发现一个更过瘾的技能：不是自己证明，而是让 Lean4 在十万条已证定理中自动帮你搜索那把丢失的钥匙。

参考资料

引用来源表

原始链接列表

https://leanprover.github.io/theorem_proving_in_lean4/tactics.html
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Ring/Basic.html
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Linarith.html

第 13 章：巨人的军火库——漫游 Mathlib

想象一座图书馆。

不是普通的图书馆。这座图书馆里有超过十万条已经被严格证明的数学定理——从最基础的自然数算术到高等微积分、代数拓扑、范畴论。每一条定理都经过 Lean4 编译器的验证。每一个证明步骤都有据可查。没有一丝含糊，没有一处"留给读者证明"。

这就是 Mathlib——人类历史上最庞大、最严格的形式化数学代码库。

而你要做的，不是从零开始构建自己的定理库。你要做的，是在这座图书馆里找到你需要的那本书、那一页、那一行。

学会搜索比学会证明更重要

这句话听起来也许有点反直觉。你花了十二章学习如何手工证明，现在我告诉你搜索比证明更重要？

是的。在真实的 Lean4 项目中，你大部分时间不是在从零证明全新的定理。你是在将已知的定理组合和拼接成你需要的结论。Mathlib 就是你的弹药库——它里面有你需要的绝大多数弹药。你不需要自己造子弹，你只需要找到正确的那颗。

问题是：超过十万条定理，怎么找？

exact?——让 Lean4 替你搜索

exact? 是一个搜索型策略。当你不知道该用哪条定理来结案时，你可以把它放在 Goal 上，Lean4 会自动在 Mathlib 和你当前的 Context 中搜索能直接匹配 Goal 的定理。

example (n : Nat) : 0 + n = n := by
  exact?
  -- Lean4 可能会告诉你：Try this: exact Nat.zero_add n

你不需要记住 Nat.zero_add 这个名字。exact? 替你找到了。

apply?——反向搜索先例

apply? 和 exact? 类似，但它搜索的是可以通过 apply 适用的定理——也就是那些能把你的 Goal 变成更简单子目标的定理。

example (a b : Nat) (h : a ≤ b) : a ≤ b + 1 := by
  apply?
  -- 可能回答：Try this: exact Nat.le_succ_of_le h

apply? 就像在判例法数据库中搜索可以适用于当前案件的先例。你告诉法官"我记得有一条类似的判例"，然后法官替你在十万条判例中翻出来了。

搜索的实际工作流

在真实的 Lean4 开发中，搜索定理的工作流通常是这样的：

第一步，写出你要证明的目标。看 Infoview 面板，确认 Goal 的确切类型。

第二步，尝试 exact?。如果运气好，它直接找到了一条匹配的定理。复制它建议的代码，替换掉 exact?，编译通过。

第三步，如果 exact? 找不到直接匹配，试 apply?。它可能找到一条能把目标简化的定理，给你一个更简单的子目标去证明。

第四步，如果自动搜索都失败了，去 Mathlib 的在线文档手动搜索。通常搜索关键词是 Goal 中涉及的核心函数或类型名——比如搜索 "Nat.add_comm" 来找加法交换律。

第五步，如果 Mathlib 里确实没有你需要的引理，那你需要自己证明它——用前面学过的策略手工完成。然后考虑是否值得贡献给 Mathlib 社区。

一个完整的搜索例子

假设你需要证明：a + b = b + a（自然数加法交换律）。

你知道这肯定是一条已经被证明过的定理——不可能没有人在 Mathlib 里证明过加法交换律。但你不知道它叫什么名字。

example (a b : Nat) : a + b = b + a := by
  exact?
  -- 回答：Try this: exact Nat.add_comm a b

搞定。Nat.add_comm 就是加法交换律在 Mathlib 中的名字。你不需要背诵它——遇到的时候搜一下就行。

随着你使用 Lean4 的时间增长，你会逐渐记住一批常用定理的名字——就像一个律师逐渐熟悉了常用的法律条文编号。但在此之前，exact? 和 apply? 就是你的检索引擎。

Mathlib 的命名规范

Mathlib 的定理命名有一套严格的规范。一旦你理解了这套规范，你甚至可以"猜"出定理的名字：

类型名 + 下划线 + 操作名 + 下划线 + 特征

比如：

• Nat.add_comm：Nat 类型上的加法 (add) 交换律 (comm)
• Nat.mul_assoc：Nat 类型上的乘法 (mul) 结合律 (assoc)
• List.length_append：List 类型上的 length 函数与 append 操作的关系
• Nat.le_of_lt：从小于 (lt) 推出小于等于 (le) 的定理

一旦你掌握了这个命名模式，很多时候你可以直接猜出定理名、在编辑器里输入然后看看有没有自动补全——这比等待 exact? 的搜索结果更快。

关于"依赖外部库不安全"

如果你是一个习惯了"减少外部依赖"的工程师，你可能会对 Mathlib 的大量使用感到不安："依赖这么一个巨大的外部库，会不会引入 bug？"

在普通的软件工程中，这种担心是合理的——第三方库的代码质量参差不齐，你无法保证每一行都没 bug。

但 Mathlib 是一个特殊的存在。它的每一条定理、每一行证明，都必须通过 Lean4 编译器的验证才能被合并。编译器不是做人工代码审查——它是做数学证明检查。如果证明有任何漏洞，编译就不会通过，代码就不会被合并。

Mathlib 的正确性保障不来自人工审查（虽然也有），而来自编译器的绝对裁决。这是形式化数学库和普通软件库之间的根本区别。

实践：用 exact? 解题

试试用 exact? 策略来解决以下问题，不要自己手工证明：

-- 1. 加法结合律
example (a b c : Nat) : (a + b) + c = a + (b + c) := by
  exact?

-- 2. 乘法分配律
example (a b c : Nat) : a * (b + c) = a * b + a * c := by
  exact?

-- 3. 零乘
example (n : Nat) : 0 * n = 0 := by
  exact?

让 Lean4 在十万条定理中替你搜索。感受站在巨人肩膀上的感觉。

接下来，我们将把本书教过的所有技能——策略、归纳法、自动化、Mathlib 搜索——全部集中起来，完成一项壮举：证明素数有无限多个。

参考资料

引用来源表

原始链接列表

https://github.com/leanprover-community/mathlib4
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Find.html
https://leanprover-community.github.io/contribute/naming.html

第 14 章：欧几里得的复活——Vibe Coding 巅峰实战

公元前300年左右，欧几里得在他的《几何原本》中给出了一个堪称人类理性之巅的证明：素数有无限多个。

那个证明的核心思路优雅到令人窒息：假设素数只有有限个。把它们全部乘起来再加 1。这个新数不能被任何已知素数整除——因为除以任何一个已知素数都余 1。这意味着它要么自身是素数，要么有一个不在列表中的素因子。无论哪种情况，都跟"素数只有有限个"矛盾。

2300年后的今天，你要让一台计算机的编译器亲自确认这个证明。

开局：坦白你不知道

让我们做一个思想实验。假设你是一个不熟悉数论的程序员。你知道素数的定义——大于1且只能被1和自身整除的数——但你不知道怎么证明它们有无限多个。

这正是 Vibe Coding 的理想起点。你不需要是数论专家。你只需要会和 AI 交流、会读编译器的报错、会使用前面学过的策略。

第一步：向 AI 询问证明思路。

Prompt："我需要在 Lean4 中证明'素数有无限多个'。请不要直接给代码。请先用自然语言描述证明策略，列出关键步骤和需要的引理。"

AI 大概会告诉你欧几里得的经典思路：反证法。假设素数有限，构造所有素数的乘积加 1，推出矛盾。

拆解为子引理

根据 AI 给出的思路，一个合理的拆解方式是：

引理一：对于任何自然数 n 和素数 p，如果 p 整除 n!+1 且 p 整除 n!，那么 p 整除 1。

引理二：没有大于 1 的自然数能整除 1。

引理三：对于任何 n，存在一个大于 n 的素数。

从引理三可以推出素数有无限多个——因为对于任意大的 n，你总能找到一个更大的素数。

在 Mathlib 中寻找弹药

在你开始手工证明每一条引理之前，先让 Mathlib 看看它已经有了什么。

-- 关于阶乘的基本性质
#check Nat.factorial_pos  -- n! > 0
#check Nat.dvd_factorial   -- 如果 1 ≤ k ≤ n，那么 k | n!

-- 关于素数的基本性质  
#check Nat.Prime            -- 素数的定义
#check Nat.minFac           -- 最小素因子
#check Nat.minFac_prime     -- 大于1的数的最小因子是素数

Mathlib 已经为你准备了大量弹药。你不需要证明阶乘的基本性质或素数的基本定义——前人已经做了这些工作。你只需要找到它们、组合它们。

证明核心：存在大于 n 的素数

以下是一种简化的证明思路，展示在 Lean4 中如何组合策略和 Mathlib 定理：

theorem exists_infinite_primes (n : Nat) : ∃ p, p > n ∧ Nat.Prime p := by
  -- 考虑 n! + 1
  let m := Nat.factorial n + 1
  -- m > 1，所以它有一个最小素因子 p
  have hm : m > 1 := by
    have : Nat.factorial n > 0 := Nat.factorial_pos n
    omega
  -- 取 p 为 m 的最小素因子
  let p := Nat.minFac m
  use p
  constructor
  · -- 证明 p > n
    by_contra h
    push_neg at h
    -- 如果 p ≤ n，那么 p | n!
    have hp_prime := Nat.minFac_prime (by omega : m ≠ 1)
    have hp_dvd_m := Nat.minFac_dvd m
    have hp_dvd_fac : p ∣ Nat.factorial n := by
      exact Nat.dvd_factorial.mpr ⟨hp_prime.pos, h⟩
    -- 但 p | m = n! + 1，所以 p | 1，矛盾
    have : p ∣ 1 := by
      have := Nat.dvd_sub' hp_dvd_m hp_dvd_fac
      simp at this
      exact this
    exact Nat.Prime.one_lt hp_prime |>.not_le (Nat.le_of_dvd one_pos this)
  · -- 证明 p 是素数
    exact Nat.minFac_prime (by omega : m ≠ 1)

这段代码中你可以看到前面学过的所有技术的汇合：use 提交存在性证据、constructor 拆分合取目标、by_contra 做反证法、omega 处理算术推理、Mathlib 定理的搜索和应用。

红绿灯闭环的真实记录

在实际操作中，上面那段代码不会是一次性写出来的。真实的过程更像这样：

第一轮：你让 AI 给出完整代码。编译器报错——某个 Mathlib 引理名不对。你把报错投喂回 AI。

第二轮：AI 修正了引理名。编译器在另一处报错——某个类型不匹配。你再投喂。

第三轮：AI 调整了类型转换。还有一个子目标没被消灭。你自己看 Infoview 面板，发现需要补一步 simp。

第四轮：所有 Goal 消失。编译通过。

这四轮往返可能在十分钟内完成。你花十分钟完成了一个 2300 年前的数学家花了不知多长时间构思的证明——不是因为你比欧几里得更聪明，而是因为你站在 Mathlib 十万条定理的肩膀上，有 AI 辅助构思，有编译器做终极裁决。

这不是作弊

也许有人会说："你不是自己证明的，你用了 AI 和 Mathlib，这算什么？"

这种说法混淆了两件事：理解和验证。

你可能不理解每一条 Mathlib 引理的内部证明。但编译器通过了。编译器验证了你的证明的每一步、每一个引理的正确性、每一个逻辑连接的严密性。

在形式化证明的世界里，重要的不是"谁写的"，而是"编译器是否通过了"。通过就是通过。数学不在乎你的证明是灵感涌现还是暴力搜索。它只在乎逻辑上是否无懈可击。

你是检察官，AI 是辩护律师，Mathlib 是判例法数据库，编译器是法官。法官说通过了，这个案件就是铁案。不接受上诉。

实践：尝试证明"合数有素因子"

作为热身练习，试着证明一个稍微简单的定理：

-- 每个大于1的自然数都有一个素因子
theorem exists_prime_factor (n : Nat) (h : n > 1) : ∃ p, Nat.Prime p ∧ p ∣ n := by
  use Nat.minFac n
  constructor
  · exact Nat.minFac_prime (by omega)
  · exact Nat.minFac_dvd n

这道题可以直接用 Mathlib 的 minFac 相关引理秒杀。但请在编辑器中亲手敲一遍，体验从搜索到组合到编译通过的完整流程。

在最后一章，我们将迎来全书的终极挑战——不再证明数学定理，而是证明一个程序的正确性。用 Lean4 编写一个排序算法，然后用数学证明它"绝不可能出错"。

参考资料

引用来源表

原始链接列表

https://mathshistory.st-andrews.ac.uk/Biographies/Euclid/
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime/Basic.html
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Factorial/Basic.html

第 15 章：代码的圣杯——编写"绝不可能出错"的程序

这是加冕时刻。

在过去的十四章中，你证明了数学等式、逻辑命题、集合定律、素数的无限性。但一个声音可能一直在你心底挥之不去："这些数学证明很酷，但和我每天写的业务代码有什么关系？"

本章将回答这个问题。你将用 Lean4 编写一个排序算法——不是用测试验证它，而是用数学证明它。证明什么？两件事：

第一，输出的列表一定是有序的。

第二，输出的列表包含且仅包含原列表的所有元素——一个都不多，一个都不少。

当这两条证明通过编译的那一刻，你拥有的不是"跑了一千个测试用例都没出错"的统计信心——你拥有的是"在所有可能的输入上都不可能出错"的数学确定性。

超越 TDD

测试驱动开发说：先写测试，再写实现，确保测试通过。

形式化验证说：先写契约（类型和命题），再写实现和证明，确保编译通过。

TDD 的覆盖范围取决于你能想到多少测试用例。形式化验证的覆盖范围是"所有可能的输入"——因为它是数学证明，不是统计抽样。

这就是那条从"大概正确"到"绝对正确"的鸿沟。让我们跨过去。

插入排序的 Lean4 实现

我们选择插入排序，因为它足够简单——你可以用十行代码实现它——但又足够复杂，能够展示形式化验证的完整流程。

首先，定义插入操作：

def insert (x : Nat) : List Nat → List Nat
  | [] => [x]
  | y :: ys =>
    if x ≤ y then x :: y :: ys
    else y :: insert x ys

然后，定义排序函数：

def insertionSort : List Nat → List Nat
  | [] => []
  | x :: xs => insert x (insertionSort xs)

两个函数。总共不到十行。逻辑很清楚：空列表已经有序；非空列表取出头元素，递归排序剩余部分，然后把头元素插入到已排序的列表中。

#eval insertionSort [5, 3, 1, 4, 2]
-- 输出 [1, 2, 3, 4, 5]

看起来工作正常。但"看起来"不够。

性质一：输出是有序的

首先定义"有序"是什么意思：

def Sorted : List Nat → Prop
  | [] => True
  | [_] => True
  | x :: y :: rest => x ≤ y ∧ Sorted (y :: rest)

一个列表是有序的，当且仅当：空列表有序（平凡成立）；单元素列表有序（平凡成立）；多元素列表中每对相邻元素满足前者小于等于后者，且剩余部分也有序。

现在，证明我们的排序函数输出的列表总是有序的：

theorem insert_sorted (x : Nat) (xs : List Nat) (h : Sorted xs) :
    Sorted (insert x xs) := by
  induction xs with
  | nil => simp [insert, Sorted]
  | cons y ys ih =>
    simp [insert]
    split
    · -- x ≤ y 的情况
      constructor
      · assumption
      · exact h
    · -- x > y 的情况
      cases ys with
      | nil =>
        simp [insert, Sorted]
        omega
      | cons z zs =>
        simp [Sorted] at h ⊢
        constructor
        · exact h.1
        · exact ih h.2

theorem insertionSort_sorted (xs : List Nat) :
    Sorted (insertionSort xs) := by
  induction xs with
  | nil => simp [insertionSort, Sorted]
  | cons x xs ih =>
    simp [insertionSort]
    exact insert_sorted x (insertionSort xs) ih

这段代码可能是你目前看到的最长的证明。但拆开来看，每一步都是你已经学过的技术：induction 做结构归纳、simp 做自动化简、split 分处理条件分支、omega 处理算术、constructor 拆分合取目标。

编译通过。你刚才数学证明了：对于任何输入列表，insertionSort 的输出一定是有序的。不是"测了一万个用例都没出错"。是"数学上不可能出错"。

性质二：不丢不增

排序算法不能丢失元素，也不能凭空产生元素。输出列表必须是输入列表的一个排列（Permutation）。

定义排列的一种方式是：两个列表是排列关系，当且仅当它们包含完全相同的元素且每个元素出现的次数相同。

-- 简化版：使用计数等价来表示排列关系
def isPerm (xs ys : List Nat) : Prop :=
  ∀ n, xs.count n = ys.count n

证明排序保持排列关系的核心思路是：insert x xs 和 x :: xs 包含相同的元素（只是位置不同），而 insertionSort 递归地对每个元素做 insert。

theorem insert_perm (x : Nat) (xs : List Nat) :
    isPerm (insert x xs) (x :: xs) := by
  intro n
  induction xs with
  | nil => simp [insert, List.count]
  | cons y ys ih =>
    simp [insert]
    split
    · simp [List.count]
    · simp [List.count]
      omega

theorem insertionSort_perm (xs : List Nat) :
    isPerm (insertionSort xs) xs := by
  induction xs with
  | nil => intro n; simp [insertionSort]
  | cons x xs ih =>
    intro n
    have h1 := insert_perm x (insertionSort xs) n
    have h2 := ih n
    simp [insertionSort]
    omega

编译通过。你刚才数学证明了：对于任何输入列表，insertionSort 的输出是输入的排列——不丢数据、不多数据。

这不是学术玩具

也许你仍然觉得这种技术离日常工程很远。让我给你几个正在发生的真实案例：

Amazon Web Services 的 s2n-tls 库——一个加密协议实现——使用了形式化验证来保证其核心密码学操作的正确性。当你通过 HTTPS 访问 Amazon 时，你的数据安全部分依赖于数学证明而非测试。

Microsoft Research 的 EverCrypt 项目用 F*语言（与 Lean4 理念相近）形式化验证了一系列密码学原语。这些经过验证的代码被用在 Firefox 浏览器和 Linux 内核中。

CompCert 是一个经过形式化验证的 C 编译器。它的正确性不是通过测试保证的，而是通过 Coq 定理证明器的数学证明保证的。CompCert 已通过航空安全标准 DO-178B 的认证，可用于航空电子等安全关键领域。

这些不是学术研究中的概念验证。这些是在生产环境中运行的、保护着数十亿用户数据和生命安全的真实系统。

你刚才做的事情——用 Lean4 证明排序算法的正确性——和这些工业级应用用的是完全相同的方法论。

类型即契约，证明即保障

让我们最后一次审视这个公式。

在 Python 中，函数签名 def sort(lst: List[int]) -> List[int] 只告诉你类型信息——接收一个整数列表，返回一个整数列表。它什么也不保证。返回一个空列表？没问题。返回一个乱序列表？没问题。返回一个和输入完全无关的列表？没问题。类型系统不管。

在 Lean4 中，你可以把函数签名写成：

def verifiedSort (xs : List Nat) :
    { ys : List Nat // Sorted ys ∧ isPerm ys xs }

这个类型签名说的是："给我一个列表，我返回一个列表 ys，且我保证 ys 是有序的，且 ys 是输入的排列。" 这个保证不是写在注释里的美好愿望，不是文档中的口头承诺——它是类型系统的一部分。如果你的实现违反了任何一条保证，代码无法编译。

类型即契约。证明即保障。

这是编程能达到的最高形式。你写的不再只是指令。你写的是一份附带数学保障书的契约。

恭喜。你已经走完了全部旅程。

参考资料

引用来源表

原始链接列表

https://github.com/aws/s2n-tls
https://hacl-star.github.io/HaclValeEverCrypt.html
https://compcert.org/
https://softwarefoundations.cis.upenn.edu/vfa-current/Sort.html

后记：代码尽头的哲学

你走到了这里。

十五章前，你是一个 Python 程序员，相信测试覆盖率是软件质量的最高标准。你知道 AI 能帮你写更多代码，但你隐隐感到那些代码的正确性正变得越来越难以把控。

现在，你知道了另一条路。

你知道命题就是类型、证明就是程序。你知道编译器可以做冷酷的法官、AI 可以做有用但需要监管的辩护律师。你知道 rfl、intro、apply、exact、induction、rw、simp、ring、linarith 这些策略，每一个都是你在逻辑法庭上的一把武器。你知道 Mathlib 是一座拥有十万条已证定理的判例法数据库。你亲手证明了排序算法的绝对正确性。

这些知识将如何改变你的日常工作？

算力归机器，直觉归人类

形式化验证不会替代日常编程。你明天上班写的那个 REST API 端点，大概率仍然会用 Python 或 Go 或 TypeScript。这没什么问题——并非所有代码都需要数学级别的正确性保障。

但你的思维方式已经变了。

当你定义一个函数的接口时，你会开始下意识地思考："这个函数的契约是什么？它的前置条件是什么？后置条件是什么？我能不能用类型系统来表达这些约束，而不只是写在注释里？"

当你面对一个复杂的业务逻辑时，你会开始把它拆解为更小的、可独立验证的子模块——就像你把德·摩根定律拆解为五个子引理一样。

当有人告诉你"AI 会取代程序员"时，你会微微一笑。因为你知道，AI 能生成代码的速度越快，对代码正确性验证的需求就越大。而形式化验证——让编译器充当数学法官——是目前已知的最强大的验证手段。

掌握 Lean4 的程序员不会被 AI 取代。他们会成为 AI 的审判者。

在 Mathlib 社区留下你的烙印

如果这本书点燃了你对形式化数学的兴趣，Mathlib 社区是你的下一个目的地。

Mathlib 的 Zulip 聊天室是全球 Lean4 爱好者的聚集地。那里有从本科生到菲尔兹奖得主的各种人。他们友善、耐心、对新人开放。

你可以从以下方式参与：

修复一个标记为"good first issue"的 Pull Request。形式化一条你在某本教科书中看到的定理。改进一条已有定理的证明——让它更短、更优雅。

每一个被合并的 PR，都意味着你的逻辑推理永久地成为了人类数学知识库的一部分。它不是写在某个容易遗忘的博客里的个人笔记——它是经过编译器验证的、不可伪造的数学真理。

最后的话

2300年前，欧几里得用纸笔证明了素数有无限多个。

今天，你让一台机器用绝对严密的逻辑重新验证了这个证明。

这不是终点。这是起点。

代码的尽头是数学。数学的尽头是哲学。而哲学的尽头——如果有尽头的话——也许是一段编译器输出的寂静。

没有 Goal。没有报错。

只有通过。

推荐资源