Lean 的逻辑基础真的有问题吗？

2026 年 10 月 9 日，Thomas Hales 在《What’s new》发表了一篇关于 Lean 可靠性的客座文章。他指出，Lean 类型论中的一些基本性质仍缺少完整证明。这颇令人意外。

本文在 GPT 和 Codex 的辅助下完成资料查证、讨论和改稿。我试图弄清楚 Lean 的理论基础是什么，现有的验证结果覆盖到了哪里，以及还有哪些问题尚未解决。

我目前的理解是，这些问题中最“严重”的是定义相等的不可判定性。但不可判定性本身不妨碍可靠的证明检查。有些类型转换在理论上成立，算法却无法确认。相应的证明项便无法通过检查。检查算法的可靠性（soundness） 要求的是：凡是检查器接受的证明，都符合规定的规则。¹

Hales 提到的类型唯一性、 $\Pi$ 单射性等，是另外一些仍需研究的元理论性质。但这些未证明的性质，并不妨碍通过其他路线建立可靠性保证。²

Upshot（我的理解）：就理论基础而言，Lean 的可靠性（soundness）并没有实质性的问题。

以下关于研究进展的判断截至 2026 年 10 月 19 日。资料和核对过的源码修订见参考资料一节。

项、类型与内核

项（term）是按 Lean 核心语言的构造规则形成的有限表达式。它的基本形式如下。这里 $x$ 表示变量， $c$ 表示已声明的常量， $u$ 表示给类型分层的宇宙层级； $t,s,A,B$ 都表示项。常量可带宇宙实参 u1, ..., un。记号 ::= 表示“由以下形式构成”，竖线表示“或”。右侧注释说明各个构造的含义。³

t ::= x                      -- 变量引用
    | c.{u1, ..., un}         -- 常量及其宇宙实参
    | Sort u                 -- 第 u 层宇宙
    | t s                    -- 函数应用：把参数 s 传给 t
    | fun (x : A) => t        -- 函数抽象：构造匿名函数
    | (x : A) → B            -- 函数类型：B 可依赖 x
    | let x : A := s; t       -- 局部定义：在 t 中令 x 为 s

这些构造规则可以反复使用，由已有的项组成更大的项。自然数与字符串的字面量、结构的字段投影，也都是项的构造形式。 Lean 用项统一表示数学对象、类型、命题与证明；类型判断 $t:A$ 中的 $t$ 和 $A$ 都是项。类型检查进一步确定一个项是否具有合法类型。

Lean 的官方内核（kernel）用 C++ 实现。 Lean4Lean 则是用 Lean 4 编写的内核实现，其代码以官方 C++ 内核的实现为基础。本文讨论具体实现时，未另注明的“内核”指官方 C++ 内核；其他检查器另行标明名称。内核用数据结构表示项和宇宙层级，并用环境保存全局声明。它按照 Lean 类型论的规则检查这些数据。它是证明助手（proof assistant）中必须保证正确的逻辑核心。

内核的三个基本操作是：⁴

类型推断：求出项的类型。
归约：按计算规则化简项。相对于给定的规则，整个项及其各个子项都已无法继续归约时，称它为规范形（normal form）。内核常用的弱头规范形（weak head normal form，WHNF） 只要求头部已无可执行的归约；例如，未应用的函数可以保留尚未化简的函数体。类型检查与相等比较会按需要进入子项继续处理。⁵
定义相等检查：判断两个项是否按照内核的计算与转换规则相等。这种相等称为定义相等（definitional equality）。内核据此比较推断出的类型与声明要求的类型，具体规则见定义相等与证明无关性一节。

一句话来说，内核的任务是做类型判断，类型判断写成 $E;\Gamma\vdash t:A.$ $E$ 是全局环境， $\Gamma$ 保存当前的变量与假设；这个判断表示在这些条件下，项 $t$ 具有类型 $A$ 。

设定理的目标命题为 $P$ ，证明项为 $p$ 。内核在已有环境中按以下步骤检查：

检查目标命题：检查 $P$ 的类型，经过必要的归约，确认 $P$ 属于 Prop。
检查证明项：检查 $p$ 并推断它的类型 $Q$ ，过程中按需归约。
核对证明目标：检查推断出的 $Q$ 与目标 $P$ 是否定义相等。通过后将定理加入环境；检查失败则报告错误。

类型推断、归约和定义相等检查在这个过程中交替使用。内核同时检查名称、宇宙参数和变量绑定等声明条件。⁶

记号（notation）的解析与展开、策略（tactics）的执行，由内核之外、用 Lean 编写的前端程序完成。这些程序称为元程序（metaprogram），即操作程序的程序；编写这样的程序称为元编程（metaprogramming）。它们把用户写下的源代码转换成核心声明，交给内核检查。 解析（parsing）按语法规则识别文本，得到语法树（syntax tree）。语法树用树状数据记录各个语法成分的组合方式。完成这一步的程序叫解析器（parser）。 精化（elaboration）把语法树转换成核心语言中的表达式和声明。完成这一步的程序叫精化器（elaborator）。它要确定名称指向哪个对象，补齐省略的参数，翻译模式匹配，并运行策略构造证明项。

定义、定理陈述和允许的公理都要先核对清楚。在这个前提下，策略中的 bug 不会破坏证明检查的可靠性。只要内核工作正确，不合法的证明项就通不过检查。⁷ 元编程的具体写法和实现，我们计划在后续文章中讨论。

依赖类型与宇宙

Lean 的类型论采用归纳构造演算（Calculus of Inductive Constructions，CIC）的一种变体。⁸ Lean 允许类型的表达式包含项参数，类型因而可以随参数变化，这称为依赖类型（dependent type）。例如，Lean 的 Vector Nat n 表示长度为 n、元素为自然数的向量类型，其中长度 n 是一个自然数参数。⁹ Vector Nat : Nat → Type 接受一个长度，返回相应的向量类型。 (n : Nat) → Vector Nat n 是依赖函数类型：函数接受自然数 n，返回长度为 n 的向量。一般写作 $\Pi x:A.\,B(x)$ ，其中 $B(x)$ 是依赖于参数 $x:A$ 的返回类型。普通函数类型 $A\to B$ 是 $B$ 不依赖 $x$ 的情形。

内核按宇宙规则检查类型的形成。Lean 用宇宙（universe）表示类型的类型，写作 $\mathrm{Sort}\,u$ ； $u$ 是宇宙层级。基本规则是： $\mathrm{Prop}=\mathrm{Sort}\,0,\qquad \mathrm{Type}\,u=\mathrm{Sort}(u+1),\qquad \mathrm{Sort}\,u:\mathrm{Sort}(u+1).$ $\mathrm{Prop}$ 就是 $\mathrm{Sort}\,0$ 的记号，表示命题所在的宇宙； $\mathrm{Type}\,u$ 是 $\mathrm{Sort}(u+1)$ 的记号。

依赖函数类型的形成规则同时给出它的宇宙层级： $\frac{\Gamma\vdash A:\mathrm{Sort}\,u \qquad\Gamma,x:A\vdash B(x):\mathrm{Sort}\,v} {\Gamma\vdash(\Pi x:A.\,B(x)):\mathrm{Sort}(\operatorname{imax}(u,v))}.$ 先确认定义域 $A$ 是类型，再假设 $x:A$ ，检查 $B(x)$ 是否为类型。这两步通过后，就能形成依赖函数类型。它的宇宙层级由下式决定： $\operatorname{imax}(u,v)= \begin{cases} 0,&v=0,\\ \max(u,v),&v\gt 0. \end{cases}$ 当每个 $B(x)$ 都是命题时， $v=0$ 。此时，依赖函数类型 $\Pi x:A.\,B(x)$ 也属于 Prop，表示全称命题 $\forall x:A,\ B(x)$ ，即对每个 $x:A$ ，命题 $B(x)$ 都成立。无论定义域位于哪一层宇宙，这样的全称量化得到的仍是命题；这就是 Prop 的非直谓性（impredicativity）。当 $v\gt 0$ 时，依赖函数类型的宇宙层级为 $\max(u,v)$ 。¹⁰

归纳类型的构造规则见归纳类型一节；商类型的规则见常用公理一节。

定义相等与证明无关性

本文用 $a\equiv b$ 表示项 $a$ 与 $b$ 定义相等，符号 $\equiv$ 读作“定义相等”。内核在类型检查时用定义相等来比较类型：如果 $A\equiv B$ ，一个类型为 $A$ 的项就可以用于要求 $B$ 的地方。

命题等式（propositional equality） $a=b$ 是 Lean 表达式 Eq a b 的记号。对于同一类型中的 $a,b$ ，Eq a b : Prop；证明这条等式就是构造一个项 h : Eq a b。 Eq 的归纳声明写在 Lean 核心库的 Init/Prelude.lean 中。内核用通用的归纳类型机制检查这个声明，并通过类型检查验证等式的证明项。¹¹

按归约规则计算项称为求值（evaluation）。内核使用以下几类操作：¹²

函数应用（β 归约）：把实参代入函数体，例如 $(\lambda x.\,x)\,a$ 化为 $a$ 。
定义展开（δ 归约）：把已定义的常量替换为它的定义体。
递归器计算（ι 归约）：当参数的构造子已知时，使用对应的计算分支；例如自然数递归分别处理零与后继。构造子将在归纳类型一节随归纳类型一起介绍。
局部定义（ζ 归约）：把 let 的定义值代入主体，例如 let x := a; x 化为 $a$ 。
投影归约：从已构造的结构中取出字段，例如 (a, b).1 化为 $a$ 。
商归约：将提升到商上的函数作用于由代表元构造的商元素时，化为原函数作用于该代表元；商类型见常用公理一节。

β、ζ 归约中的变量代换（substitution）保持变量的绑定关系。

以自然数加法为例。Nat 的构造子是零和后继 Nat.succ。 Nat.add 的定义对第二个参数递归，给出以下计算规则：¹³

Nat.add a 0            ↦ a
Nat.add a (Nat.succ b) ↦ Nat.succ (Nat.add a b)

对变量 n : Nat，n + 0 直接按第一条规则归约为 n。两边定义相等，因此命题等式可以用 rfl 证明：

example (n : Nat) : n + 0 = n := rfl

上例中的 rfl 是核心库定义的反身性证明，精化器补齐其隐式参数。反身性证明 Eq.refl n 的类型是 Eq n n；内核确认它与目标 Eq (n + 0) n 定义相等，于是接受这个证明。

0 + n 的第二个参数是未知的 n，递归器还无法选择零或后继分支。它与 n 不定义相等。对目标 0 + n = n 执行策略 by rfl，会在精化阶段报错：¹⁴

Tactic `rfl` failed: The left-hand side
  0 + n
is not definitionally equal to the right-hand side
  n

这条命题等式由归纳证明的定理 Nat.zero_add 给出：

example (n : Nat) : 0 + n = n := Nat.zero_add n

内核在这里检查 Nat.zero_add n 的类型是否为 Eq (0 + n) n。

Lean 将证明无关性（proof irrelevance）直接规定为定义相等的一条基本规则：同一命题的任意两个证明都定义相等。官方 C++ 内核和 Lean4Lean 都实现了这条规则，在比较证明时检查它们所属的命题，忽略证明的具体构造。¹⁵ 把一个数和它满足某条件的证明放在一起时，更换证明不会改变这个对象。

内核还规定了命题的消去限制。比如存在命题的证明，一般不能通过模式匹配就提取成可计算数据。¹⁶ 关于命题等式 Eq 及其相关规则，我们会另开一篇博客讨论。

归纳类型

inductive 命令的元程序读取类型名称、宇宙和构造子等信息，生成一份归纳声明，提交给内核。 归纳类型机制由内核实现：内核检查收到的声明，将类型和构造子加入环境，并生成递归器及其计算规则。¹⁷

以核心库中的 inductive Nat 为例，完成这一步后，环境中有以下类型和构造子：

Nat      : Type
Nat.zero : Nat
Nat.succ : Nat → Nat

从依赖类型论的角度看，Nat 是一个新引入的类型常量，其类型是 Type，即 Sort 1。核心项中的 Nat 就是对这个常量的引用。这个类型由归纳类型的形成规则引入。¹⁸

构造子（constructor）规定怎样构造这个类型的值。 Nat.zero : Nat 本身就是零；Nat.succ : Nat → Nat 是接受自然数并构造其后继的函数。例如，下面三个项分别表示零、一和二：

Nat.zero                         -- 0
Nat.succ Nat.zero                -- 1
Nat.succ (Nat.succ Nat.zero)     -- 2

这些生成规则给出了归纳类型（inductive type）的构造方式。

递归器（recursor） Nat.rec 按零和后继两种情形定义函数或证明命题。它的类型可写成下面的形式，这里用 P 命名目标类型族：

Nat.rec :
  {P : Nat → Sort u} →
  P Nat.zero →
  ((n : Nat) → P n → P (Nat.succ n)) →
  (n : Nat) → P n

P 为每个自然数 n 指定一个返回类型 P n。先给出零处的值。再说明：已知类型为 P n 的值，怎样构造类型为 P (Nat.succ n) 的值。有了这两项，Nat.rec 就能为每个 n 生成类型为 P n 的结果。这里的 (n : Nat) → P n 是依赖函数类型：返回类型随输入 n 变化。

当 P : Nat → Prop 时，Nat.rec 的用法就是数学归纳法。先证明 P 0，再证明归纳步骤：对任意 n，由 P n 推出 P (Nat.succ n)。 Nat.rec 把这两部分组合成 (n : Nat) → P n 的证明。从 Lean 的实现看，这条归纳准则由 Nat 的归纳定义自动给出。

常用公理

内核负责接纳公理声明。它先检查声明的类型。检查通过后，就把一个具有该类型、没有定义体的常量加入环境。源码中的 axiom 命令将公理声明提交给内核。¹⁹

下面是 Lean 核心库中三条常用公理的具体声明。

propext 是命题外延性公理：

axiom propext {a b : Prop} : (a ↔ b) → a = b

它接受两个命题互相蕴含的证明，给出命题等式 a = b 的证明。²⁰

Quot.sound 给出商类型中的等式：

axiom Quot.sound.{u} {α : Sort u} {r : α → α → Prop}
    {a b : α} : r a b → Quot.mk r a = Quot.mk r b

这里 r 是 α 上的二元关系，Quot r 是相应的商类型， Quot.mk r a 把代表元 a 送入商类型。给定 r a b 的证明，这条公理就给出两个商元素相等的证明。内核另外提供商的构造、函数提升、归纳及相应计算规则。²¹

Classical.choice 是选择公理：

axiom Classical.choice.{u} {α : Sort u} : Nonempty α → α

Nonempty α : Prop 表示 α 有元素。这条公理接受非空性的证明，并给出一个 α 中的元素。²²

在 Lean 的标准数学基础下，完成的证明至多依赖这三条公理。

#print axioms 元程序可以用来读取并显示声明的公理依赖。²³ 证明检查还依赖宇宙、转换、归纳类型和证明无关性等规则，以及检查器对这些规则的正确实现。 Mathlib 在这套基础之上组织数学定义和定理。

一致性

一套数学理论的一致性（consistency）是说：从固定的公理出发，按这套理论的推理规则，无法同时证明某个命题和它的否定。例如，Lean 可以证明自然数中的 $0\ne 1$ ；如果从同一组公理出发、按同样的规则还能证明 $0=1$ ，就得到了矛盾，这套理论也就不一致了。

Lean 用命题 False 表示矛盾。因此，一致性可以准确地表述为：仅凭选定的公理和推理规则，无法构造出一个 False 的证明项。一旦有了 False 的证明项，就可以按 Lean 的逻辑规则推出任意命题。²⁴ 讨论 Lean 的一致性时，须先固定所用的公理，例如上一节列出的三条常用公理； sorry 所调用的占位公理不在其中。²⁵

证明一致性的一种办法，是给类型、项和命题建立数学模型：让公理在这个模型中成立，并证明每条推理规则都把成立的前提变为成立的结论。这样就能保证，凡是按规则证明的命题，在这个模型中都成立；这称为相对于该模型的可靠性（soundness）。只要 False 在这个模型中为假，就能推出它无法被证明。

类型判断的猜想

《Lean4Lean》第三版 §2.4 列了三个猜想：2.7、2.9 和 2.10。它们研究抽象类型论的推导关系，以及这些关系如何支持检查程序的正确性证明。

猜想 2.7：类型唯一性。 类型唯一性要求：同一个核心项在同一上下文中若有两个类型，那么这两个类型定义相等。 $\Gamma\vdash t:A,\quad\Gamma\vdash t:B \quad\Longrightarrow\quad \exists u,\;\Gamma\vdash A\equiv B:\mathrm{Sort}\,u.$ 如果猜想成立，正确的类型推断程序所给出的类型，就应与任何合法推导得到的类型定义相等。
猜想 2.9(1)：Sort 单射性。 Sort 单射性要求：若 $\Gamma\vdash\mathrm{Sort}\,u\equiv\mathrm{Sort}\,v$ ，则层级 $u$ 与 $v$ 等价，即给宇宙参数代入同样的自然数时，两者总得到相同的值。它保证宇宙的定义相等保留层级信息，为“把宇宙比较归结为层级比较”提供理论依据。
猜想 2.9(2)： $\Pi$ 单射性。 $\Pi$ 单射性要求：若两个依赖函数类型整体上定义相等，则参数类型以及相应上下文中的返回类型也定义相等： $\begin{gathered} \Gamma\vdash(\Pi x:A.\,B)\equiv(\Pi x:A'.\,B')\\ \Longrightarrow\quad \Gamma\vdash A\equiv A',\qquad \Gamma,x:A\vdash B\equiv B'. \end{gathered}$ 它保证函数类型的参数类型和返回类型可以确定到定义相等，支持函数应用与类型比较的验证。
猜想 2.9(3)：Sort 与 $\Pi$ 类型互异。 这条类型构造子的互异性要求 $\Gamma\not\vdash\mathrm{Sort}\,u\equiv(\Pi x:A.\,B).$ 宇宙与依赖函数类型保持不同的类型形状，因而检查器按这两种形状分别处理时，其分类可以在抽象理论中得到说明。 2.9 的三项合称定义性反演：从整体类型之间的定义相等，恢复类型构造及其组成部分的信息。²⁶
猜想 2.10：加强。 加强（strengthening）要求可以删除判断中未使用的假设。原文对不含 $\Delta$ 中变量的 $s,t$ 提出 $\Gamma,\Delta,\Gamma'\vdash s\equiv t \quad\Longleftrightarrow\quad \Gamma,\Gamma'\vdash s\equiv t.$ 这里须保持上下文合法，并正确调整变量引用。例如，一个只使用 $n:\texttt{Nat}$ 的判断，在增加无关变量 $m:\texttt{Nat}$ 后得到证明，我们希望删去 $m$ 后仍能证明它。这为简化局部上下文、分析绑定变量与代换提供保证。

在 Lean 内核的结构比较分支中，比较两个 $\Pi$ 类型或两个 $\lambda$ 项时，先比较参数类型，再在共同上下文中比较主体。检查函数应用时，完整检查分支先推断函数类型与实参类型，再比较实参类型和函数的参数类型。²⁷ 在这些分支中，参数类型的一致性来自直接比较，无需在运行时借助上述反演性质。

归约、算法相等与可判定性

规范化

规范化研究项的计算能否结束。 弱规范化要求每个被研究的项至少有一条到达规范形的归约路径；强规范化要求每条归约路径都终止。这两个问题都针对指定的项和归约规则。 Andreas Abel 与 Thierry Coquand 在 2020 年给出了反例：在他们研究的非直谓、证明无关的等式理论中，一个使用 propext 的闭合证明项会循环归约，连弱头规范形也不存在。它的类型是 $\forall P:\mathrm{Prop}.\,P\to P$ ，这是一个可以证明的命题。²⁸ 这个结果排除了在定义相等检查时使用的“先把所有项算到规范形，再比较它们”这一方案的通用性。

定义相等的不可判定性

定义相等的可判定性要求存在一个算法，对每一组合法输入都在有限时间内给出相等与否的正确答案。 Carneiro 2019 对其形式化的定义相等关系给出了否定结果，论证将不可判定的问题编码进转换判断。²⁹ 对于没有识别出的转换，程序可以拒绝输入；使用者可能需要调整表达式或提供显式的等式证明。

算法相等与类型保持

把一次具体比较程序接受的关系称为算法相等。它的行为要按实现和版本研究。 Carneiro 2019 的 §3.1.1 给出了算法比较接受 $a$ 与 $b$ 、接受 $b$ 与 $c$ ，却不接受 $a$ 与 $c$ 的情形。 2026 年官方内核的缓存修复说明也明确讨论了这种非传递性。³⁰

类型保持要求项归约后仍具有原来的类型。 Carneiro 2019 的 §3.1.2 说明，把上述算法相等直接用于类型转换规则，会出现带中间转换的项可被接受、删去中间步骤后却被拒绝的情况。³¹ 这说明表达式的改写可能改变算法检查的结果。关于抽象判断的类型保持、某个算法的接受范围，以及实际程序是否会接受错误证明，需要分别论证。

Church–Rosser 问题与合流性

一项计算通常有不止一个可以先化简的地方。 合流性要求：从同一个项 $t$ 出发，沿不同路径得到 $u$ 和 $v$ 后，还能继续归约到某个共同结果 $w$ ： $t\to^*u,\quad t\to^*v \quad\Longrightarrow\quad \exists w,\;u\to^*w\ \text{且}\ v\to^*w.$ $\to^*$ 表示零次或多次归约。例如， $(\lambda x:\texttt{Nat}.\,x)\,(1+2)$ 可以先应用外面的函数，也可以先计算参数：

同一计算的两条归约路径

先应用函数，再计算加法： $(\lambda x:\texttt{Nat}.\,x)\,(1+2)\;\to\;1+2\;\to\;3$
先计算参数，再应用函数： $(\lambda x:\texttt{Nat}.\,x)\,(1+2)\;\to\;(\lambda x:\texttt{Nat}.\,x)\,3\;\to\;3$

上述两条路径都到达 $3$ 。一般的合流性定理要对所研究的每个项、每对归约路径证明这种汇合。把归约步骤及其反向步骤连起来，可以得到一个等价关系。 Church–Rosser 性质说，这样等价的两个项总有共同归约点。它与合流性等价。它支持通过计算后的形状比较类型构造及其组成部分。

证明检查的可靠性（soundness）要求检查器接受的每个证明都符合 Lean 的逻辑规则。定义相等不可判定时，检查器仍可满足这一要求：无法确认的转换可以拒绝。内核实现中的错误则可能让非法证明通过检查。下一节的漏洞就是例子。

不同的内核实现

2026 年 7 月，Lean 内核的 #14576 可靠性漏洞（soundness bug） 使一个非法的 False 证明通过了检查。问题出在归纳声明的改写过程中。有些原始参数在辅助声明中不再出现，旧内核漏查了这些参数的类型。因此，带有类型错误的声明也通过了检查。修复补上了相应的类型检查，并于 7 月 28 日随 Lean 4.32.2 发布。³²

官方前端生成的证明，可以导出为核心声明，交给不同的内核实现复核。下表列出几种主要实现。

实现	语言	特点
官方 Lean 4 内核	C++	Lean 系统日常使用的类型检查器。
Lean4Lean	Lean	以官方算法为基础重写检查器，并开展形式化验证。
Nanoda	Rust	独立实现的外部检查器，可复核 Lean 导出的核心声明。
Con-Leche	Lean	在规定的集合论假设下，为验证模式（verified）接受的声明建立了模型保证。
Con-Ron	Rust	实现 Con-Leche 的检查算法，提供另一种运行环境下的复核。

Lean Kernel Arena 收录了多种内核（type checker）的测试与对比结果。

最后，值得一提的是，针对 Lean 内核的问题，Lean 社区还提出了内核逻辑改进计划（Lean Kernel Logic renovation）。希望减少内核中的隐式推断和启发式处理，使实现和验证更简单。

参考资料

以下是本文的主要来源，研究状态截至 2026 年 10 月 19 日。

论文与研究报告

Abel, Andreas 与 Coquand, Thierry (2020). “Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality.” Logical Methods in Computer Science 16(2)，article 14。
Carneiro, Mario (2019). The Type Theory of Lean. 硕士论文，Carnegie Mellon University。
Carneiro, Mario (2024；2025 年修订). “Lean4Lean: Verifying a Typechecker for Lean, in Lean.” arXiv:2403.14064，第三版，2025 年 9 月 14 日。
Carneiro, Mario；Coquand, Thierry；Frabetti Mathieu, Adrien； Lennon-Bertrand, Meven；Melliès, Paul-André；Weirich, Stephanie (2026). “Definitional Inversion, Without Normalisation.” arXiv:2607.13662，第一版，2026 年 7 月 15 日。
Hales, Thomas (2026). “What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI.” 《What’s new》客座文章，10 月 9 日。
Moura, Leonardo de (2026). “Postmortem for Kernel Soundness Bug #14576.” 8 月 1 日。

文档与实现

Lean Language Reference，4.35.0。
Theorem Proving in Lean 4。
Type Checking in Lean 4，ammkrn。
内核实现： Lean 4（4.35.0）、 Lean4Lean、 Nanoda、 Con-Leche、 Con-Ron。
测试与计划：Lean Kernel Arena；内核逻辑改进计划 #14977。
Rocq Reference Manual，9.2.0，Subtyping rules。

定义相等的不可判定性与算法的不完备性，见《Lean4Lean》§8；内核检查的职责与信任边界，见《Type Checking in Lean 4》的 What is the kernel? 与 Trust。↩︎
见《Lean4Lean》§2.4。该节分别讨论了避开类型唯一性的模型路线，以及验证检查算法仍需的结构性质。↩︎
构造及其含义见《Type Checking in Lean 4》的 Expressions 章。本段按 Lean 4.35.0（修订 eb6cafb）核对了 C++ 内核 src/kernel/expr.h 的构造列表。↩︎
实现见 Lean 4.35.0 的 src/kernel/type_checker.cpp； Lean4Lean 的对应实现见修订 67f63b0 的 Lean4Lean/TypeChecker.lean。↩︎
见《Type Checking in Lean 4》的 Weak and strong reduction 节； C++ 实现见 type_checker.cpp 中的 whnf 和 whnf_core。↩︎
定理检查见 src/kernel/environment.cpp； Lean4Lean 中的对应流程见 Lean4Lean/Environment.lean。↩︎
解析、精化与内核检查的分工见官方手册的 Elaboration and Compilation；生成证明的元程序与信任范围见《Type Checking in Lean 4》的 Trust 节。↩︎
见《Theorem Proving in Lean 4》§1.3。↩︎
Lean 4.35.0 中的定义见 Init/Data/Vector/Basic.lean。↩︎
Lean 的宇宙不具有累积性：低层宇宙中的类型不能直接用在要求高层宇宙的地方。宇宙多态允许同一个声明在不同宇宙层级上实例化；显式提升则为原类型构造一个位于更高宇宙的副本。 Rocq 的 Type 宇宙具有累积性（cumulativity），允许低层宇宙中的类型直接用在要求高层宇宙的地方，见Rocq 手册的 Subtyping rules。 Lean 的宇宙规则参见官方手册的 Functions 与 Universes；内核中计算函数类型宇宙层级的实现见 type_checker.cpp 的 infer_pi。↩︎
见官方手册的 Propositional Equality； Eq 的声明见 Lean 4.35.0 的 Init/Prelude.lean。↩︎
见官方手册的 The Type System 与《Type Checking in Lean 4》的 Reduction 章。 β、ζ 归约中的变量代换可对照 C++ 内核的 whnf_core。↩︎
定义见 Lean 4.35.0 的 Init/Prelude.lean。内核对具体自然数字面量的加法还有直接计算的加速实现，见 type_checker.cpp 的 reduce_nat。↩︎
证明项 rfl 的定义见 Init/Prelude.lean；策略的实现见 BuiltinTactic.lean 的 evalRefl。↩︎
见官方手册的 Propositions 中的 Definitional proof irrelevance；实现见 C++ 内核的 is_def_eq_proof_irrel，以及 Lean4Lean 的 isDefEqProofIrrel。↩︎
递归器可消去到哪些宇宙，由 C++ 内核的 elim_only_at_universe_zero 确定； Lean4Lean 的对应实现是 isLargeEliminator。↩︎
精化器构造 Declaration.inductDecl 并提交的代码见 Lean 4.35.0 的 Lean/Elab/MutualInductive.lean；内核生成递归器的代码见 src/kernel/inductive.cpp。精化器还会生成 recOn、casesOn 等辅助定义。↩︎
见官方手册的 Inductive Types，以及核心库中的 Nat 声明。↩︎
见官方手册的 Axioms；内核入口为 environment.cpp 的 add_axiom。↩︎
声明见 Init/Core.lean。↩︎
Quot.sound 的声明见 Init/Prelude.lean；内核中的商声明入口见 environment::add_quot，计算规则见 quot_reduce_rec。↩︎
Nonempty 与选择公理的声明见 Init/Prelude.lean。↩︎
实现见 Lean/Elab/Print.lean。↩︎
False 的含义与从矛盾推出任意命题的规则见官方手册的 Truth。例子中的 $0\ne 1$ 对应核心库定理 Nat.zero_ne_one。↩︎
见官方手册的 Axioms，特别是 Consistency 与 Standard Axioms。↩︎
定义性反演的作用另见《Definitional Inversion, Without Normalisation》§1 的 Definitional inversions。↩︎
见 Lean 4.35.0 的 is_def_eq_binding 与 infer_app 的完整检查分支。↩︎
见 Abel–Coquand 2020，第 14:3 页。原文给出 Lean 3.4.2 的代码；本书配套文件另核验了 Lean 4.35.0 中的定义及受限归约行为。达到资源限制的实验只核验运行行为，非规范化结论来自论文的数学论证。↩︎
见 Carneiro 2019，§3.1；《Lean4Lean》§8 也据此说明检查算法的不完备性。↩︎
历史算法关系见 Carneiro 2019，§3.1.1；实际实现的说明见 Lean #14806。本文的 $\equiv$ 表示按理论规则推导的定义相等；一次算法比较失败不构成该理论中不相等的证明。↩︎
同文 §3.1.2 用 $\mathrm{id}_A(\mathrm{id}_B\,t)$ 归约为 $\mathrm{id}_A\,t$ 说明这一点：前者逐次使用算法接受的比较，后者直接要求比较两个端点。该例的结论针对论文定义的算法型判断。↩︎
具体复现见问题报告 #14576，源码修改见修复 #14577；过程分析见 Leonardo de Moura 的 2026-08-01 复盘，修复版本见Lean 4.32.2 发布说明。↩︎

Ma Jia-Jun （马家骏）