类型检查器的可信基底：编译通过到底信什么

到第 08 篇为止，"编译通过 = 定理得证"的等式在 Lean 4 里已经成为肌肉记忆。但每个写过证明的读者迟早会问：

我相信 Lean 编译通过等价于定理得证。但这条信任传到底是信什么？

本篇专门回答这个问题。形式化方法不让人脱离信任，它让人把"信什么"明确化。明确化的边界叫可信计算基底（Trusted Computing Base，TCB）。形式化系统的 TCB 越小越好；任何 sorry、任何坏公理、任何元理论缺口都会让 TCB 撑大。

本篇按"哪些东西必须信、哪些东西不必信、信任面破口长什么样、坏公理怎样让整套系统崩"四段展开。

什么是 TCB

TCB 在安全领域指"必须正确才能保证系统安全的最小组件集合"。在形式化系统里它有一个对位的定义：

必须正确才能让"编译通过 = 定理得证"这条等式成立的最小组件集合。

对一个用 Lean 4 写出的证明，TCB 通常包括：

Lean 4 的类型检查器内核——按规则机械验证每一段良类型项。
Lean 4 内核所依赖的底层运行时——Lean 自身的求值器、Nat/String 等基础类型的内置实现。
元理论保证——Lean 4 类型理论（基于 CoC 加扩展）是一致的这件事，没有被 Lean 本身证明，被外部数学家在 ZFC 或更强系统里相信。
编译 Lean 内核的底层工具链——C++ 编译器、操作系统、CPU 指令集。
读者用 Lean 写下来的所有 axiom 声明。

TCB 之外的东西不必信：

写过的 tactic 链——它们最终展开成 term 项被内核重新检查。
写过的 def——内核会对每段定义独立验证类型。
用过的库（Mathlib4 几百万行）——只要内核接受了它，库里出 bug 不会"穿透"到内核之外。
编辑器、InfoView、补全工具——这些都是"建议器"，不参与最终判定。

de Bruijn 准则：证明系统的可信度取决于一个小内核能否独立验证全部证明。所有"辅助工具"都不在 TCB 内。
AUTOMATH（de Bruijn 1968）就是按这条准则设计的。Lean 4 继承了同样的哲学：内核约 10K 行，所有 tactic、所有 Mathlib 引理都最终接受内核独立检查。

Lean 4 的内核做什么

Lean 4 内核接受的输入是一个"环境"——一组类型声明、定义、归纳类型、定理声明加上对应项。内核做的事：

类型检查：对每条定义/定理，按类型规则一步步验证其项符合声明类型。
归一化与判等：在比较两个类型时，按 β、δ、ι、ζ 规约把表达式归一化，再做结构相等性比较。
正向性检查：对 inductive 定义，验证构造子参数中的"出现位置"是严格正向的（避免 Russell 类型悖论）。
终止性检查：对递归定义，验证是结构性递归或显式提供了良基度量。
宇宙约束求解：按宇宙变量与约束求解，避免 Girard 悖论。

这五件事走完，内核给出二选一的结论：

接受：当前环境里所有声明都通过类型检查；任何用这些声明组装的证明都自动可信。
拒绝：某条声明类型错误，对应的"证明"被丢弃。

没有第三种可能。"差不多对"或"几乎成立"在内核里不存在。

信任传递链

把"我写的证明被相信"这件事拆成一条信任传递链：

用户的 .lean 文件
    -> Lean 4 编辑器（建议器，不在 TCB）
    -> Lean 4 编译器前端 elaboration（生成 term，不在 TCB）
    -> Lean 4 内核 type-check（在 TCB）
    -> Lean 4 元理论一致性（在 TCB）
    -> 编译 Lean 的 C++ 工具链与 OS（在 TCB）

链路上每一环都可能出错。但只有标了 TCB 的几环会让"得证"这件事失效。比如：

elaboration 翻译错——产生不被内核接受的 term——内核拒绝——证明失败，被用户看到。
内核实现有 bug——把不正确的 term 误判通过——证明失败，但用户看不到，整个项目都被污染。
元理论不一致——系统能"证明" False——一切命题可证，"得证"丧失意义。

工程上 TCB 越小越好，原因正是：减小 TCB 等于减少"看不见的失败模式"。

当 `False` 可被证明时

类型理论的一致性等价于"不存在 False 的证明"。如果某种意外让 False 可证：

1
2
3

theorem disaster : False := by
  -- 由某条 bug 或坏公理推出
  sorry

那么从 False 出发可以推出任何命题：

1 2	`theorem anything (P : Prop) : P := False.elim disaster`

这意味着"1 = 0"、“黎曼猜想”、“P ≠ NP"全部"可证”。系统的"得证"不再区分真伪。

一致性是形式化系统的命根子。任何能让 False 可证的途径——内核 bug、坏公理、不良 inductive——都让整套系统对外部失去意义。

坏公理：用 `axiom` 自己埋雷

Lean 4 允许显式引入公理：

1	`axiom funext : ∀ {α β : Sort _} {f g : α → β}, (∀ x, f x = g x) → f = g`

funext（函数外延性）是 Lean 4 标准库正式接受的公理之一。它不是从类型理论推出的，而是被人为加入。

公理的代价：一旦写下 axiom，内核不再要求给出项，只接受声明的类型。Lean 不再检查"这条公理是不是与其他公理一致"，那是元理论问题。

如果不小心写下一条"看起来无害但其实不一致"的公理：

axiom bad : 1 = 2

theorem doom : False := by
  have h : 1 = 2 := bad
  exact absurd h (by decide)

整个项目里 decide 把 1 ≠ 2 自动证出，再用 bad 推出矛盾。False 一旦可证，前面所有定理与库都被污染。

axiom 是形式化系统里最危险的声明。Mathlib 的策略是：只接受被外部数学家广泛验证的少数公理（Classical.choice、propext、Quot.sound），并把每条公理的引入位置追溯到底层。

验证 Lean 4 当前使用了哪些公理可以跑 #print axioms theorem_name，例如：
1
#print axioms Nat.add_comm
输出会列出该定理依赖的全部公理。Mathlib 的库审核流程依赖这条命令做"信任面追溯"。

`Classical.choice` 与排中律

Lean 4 的 Classical 命名空间提供一组让证明变"古典"的公理：

1
2
3

axiom Classical.choice : {α : Sort u} → Nonempty α → α
theorem Classical.em : ∀ (p : Prop), p ∨ ¬p
theorem Classical.byContradiction : ∀ {p : Prop}, (¬p → False) → p

Classical.choice 是核心公理，其他都从它推出（Diaconescu 定理：选择公理推出排中律）。引入 Classical.choice 之后：

Lean 4 仍然一致（被外部相信）。
但每条用了 Classical.em 或 Classical.byContradiction 的证明都不再是构造性的——它不会提取出一个具体见证。
用 #print axioms 检查时，相关定理会显示依赖 Classical.choice。

工程含义：

写"日常数学"时大量定理本来就需要排中律（实分析、测度论、点集拓扑），不用 Classical 寸步难行。
写"可执行算法"时尽量避免 Classical，否则提取出的代码没有意义（“存在性"提不出"构造性”）。
形式化项目的可信度审核第一步就是看 #print axioms 输出，确认没引入意料之外的公理。

`sorry` 是临时记号

sorry 在 Lean 里是公理的语法糖：

1 2	`theorem todo : ∀ n : Nat, n + 0 = n := by sorry`

内部相当于 axiom sorryAx : ∀ {α : Sort u}, α。它接受任何类型。一旦使用 sorry：

Lean 输出警告。
该定理及其下游全部不可信。
#print axioms 会显示依赖 sorryAx。

Mathlib CI 强制零 sorry。读者自己的项目最好在 lakefile 里加个检查脚本拒绝 sorry 进入主分支。

内核 bug：一个真实的历史

Coq 历史上多次出现内核 bug 导致 False 可证：

Pollack 2007：通过宇宙多态绕过宇宙约束证 False。
Kirchner 2013：通过 guard condition 实现缺陷绕过良基检查证 False。
Mahboubi 2018：通过 universe inconsistency 绕过宇宙层级证 False。
Coq 8.10 时代：cumulative inductive types 早期实现存在缺陷。

每次发现都伴随修复与版本升级，且会列出影响范围——哪些版本受影响、哪些证明可能依赖该 bug。Lean 4 至今也修过类似的内核问题。

内核 bug 不让形式化方法失去价值。相反，它说明形式化把"信任面"具体化到一个小到可被持续审计的组件上。普通编译器里 bug 散落在百万行代码与若干个相互纠缠的优化 pass，几乎不可能穷举；形式化内核 10K 行，每个 bug 都能被精确定位、广泛通告、统一修复。

一致性证明：Lean 4 怎样被相信

Lean 4 的类型理论是 CoC（Calculus of Constructions）的扩展，加了归纳类型、宇宙、命题外延、商类型等。这个理论的一致性不能由 Lean 自己证明（Gödel 第二不完备定理）。它的一致性来自外部：

由 Mario Carneiro 等人在 ZFC 加 ω 个不可达基数的元理论中证明（手稿在 https://arxiv.org/abs/1908.10703）。
元理论中的论证由人类数学家审阅。
Mathlib 社区维护一份"已发现的一致性威胁"清单，任何新发现都会引发讨论。

工程上接受 Lean 4 一致性等价于接受：

ZFC 一致。
大基数公理（不可达基数）一致。
上述外部证明无人发现破绽。

这条信任链比"信编译器"长，但每一环都被广泛公开、可被独立验证。

软件供应链的可信基底

即使 Lean 内核完全正确、元理论无破绽，编译 Lean 内核的 C++ 编译器、操作系统、CPU 仍然在 TCB 内。攻击者可以：

修改 GCC，让它在编译 Lean 内核时插入恶意逻辑（Reflections on Trusting Trust）。
修改 OS 加载器，让它在加载 Lean 二进制时打补丁。
修改 CPU 微码，让特定指令在特定上下文下产生错误结果。

这些是任何软件都面临的供应链问题。形式化方法没有解决它们，但形式化把这些问题之外的所有失败模式压到了内核检查里——这是它能给出的最大保证。

CompCert 项目把这条边界又推前了一步：编译器本身经过形式化验证，因此"信 C 编译器"这一环可以被 Lean/Coq 内核验证过的二进制替代。但 Coq/Lean 内核仍然要被某个未被形式化的编译器编译。无穷回归在某一点必须停。

减小 TCB 的工程手段

形式化项目有几条实践能让 TCB 持续缩小：

手段	作用
跑 `#print axioms` 审核	定期检查关键定理依赖的公理集合
拒绝 `sorry` 进主分支	CI 里加 `grep -r "sorry" src/` 失败保护
引入的 `axiom` 单独成文件	让每条公理可被代码审查
用结构性归纳代替良基递归	减少自定义终止度量带来的审计面
把 `Classical` 局限在必要范围	区分"日常数学"与"可执行算法"
用同伦类型论或立方类型论替代 `funext`	让公理变成定理（前沿方向）
第三方独立实现内核	比如 `lean4checker` 项目，让多个内核交叉验证

工程项目里这些手段不是装饰：CompCert、seL4、Mathlib 都在持续追踪 TCB 大小，把它当成核心指标维护。

模式提炼

模式	内容
信任面有边界	形式化不消灭信任，它让信任面明确可审计
内核越小越好	de Bruijn 准则：小内核独立验证所有证明
公理是显式负债	每条 `axiom` 都扩大 TCB，需要被列入信任清单
`sorry` 是破口	临时占位即可，主分支严禁
一致性来自元理论	Lean 自己不证 Lean 一致，依赖外部数学家在更强系统中验证
TCB 持续缩小	形式化项目把"减小 TCB"当成长期工程

给读者的练习

在自己的 formal_intro 工程里跑 #print axioms Nat.add_comm，看依赖了哪些公理。
故意在一段证明里 import Classical，跑 Classical.em，观察 #print axioms 输出变化。
写一段 axiom bad : 1 = 2，再写 theorem doom : False，观察 Lean 是否警告。把这条文件单独隔离不要 import 到主项目。
读 Mario Carneiro 的 Lean 4 类型理论文档前两节，理解 Lean 4 的元理论基线在哪里。

衔接到下一篇

本篇说清楚了"编译通过"到底要信什么。下一篇换镜头，看几个真实的大型形式化案例：CompCert（验证过的 C 编译器）、seL4（验证过的微内核操作系统）、Four Color Theorem（首个用计算机辅助证明的著名数学猜想）、Mathlib4（社区驱动的大规模数学库）。每个案例都要回答：“它证了什么”、“代价是多少”、“信任面在哪里”、“对工程意味着什么”。

那一篇之后剩两篇收束：第 11 篇谈形式化方法的局限与取舍，第 12 篇把视角拉到"作为日常工具的形式化"，把读者放回真实工程。