Lean 的基础究竟是什么：读 Hales 的文章之后

2026 年 10 月 9 日，Thomas Hales 在《What’s new》发表了一篇关于 Lean 可靠性的客座文章。 最近围绕形式化数学的讨论，大多在问 AI 已经会证明什么、还能证明什么。 Hales 把问题往下追了一层：我们用 Lean 检查证明，又凭什么相信 Lean？

这个问题值得认真回答。尤其是文章提到，Lean 类型论中的一些基本性质仍没有完整证明， 其中甚至包括“一个项的类型在定义相等的意义下唯一”。 对习惯了数学教材写法的人来说，这很难不令人意外：如此基本的事情，怎么会还没有解决？

但如果读完文章，只剩下“Lean 的地基可能有问题”这一印象，也会错过重要的区别。 一份关于类型论的证明有缺口，与已经从类型论的规则推出矛盾，是两回事。 一个检查器有了可靠性证明，与整套抽象理论的所有重要性质都已证明，也不是一回事。 Hales 的文章把这些问题提到了台前；本文想接着往下讲，说明它们各自是什么， 现有结果究竟证明了什么，以及研究者正在怎样补上缺口。

以下关于研究进展的判断截至 2026 年 10 月 19 日。 资料和核对过的源码修订见文末的参考资料。 本文讨论的是这些公开结果的内容与边界，不声称重新审计了所有项目的形式化证明。

Lean 检查的究竟是什么

先看一个判断： E;\Gamma\vdash t:A. 它说，在全局声明环境 E 和局部上下文 \Gamma 中，项 t 的类型是 A。 全局环境保存已经引入的类型、定义、定理和公理；上下文保存当前的变量与假设。 当 A 是一个命题时，t 就是它的证明。

这就是“命题即类型”的具体含义。证明 P\to Q，是构造一个把 P 的证明变成 Q 的证明的函数；证明 \forall x:A,\ P(x)，是构造一个接受 x、返回 P(x) 的证明的函数。证明不只是宣告某件事成立，而是一个有待检查的数学对象。

用户通常不会把这个对象完整地写出来。数学记号、隐式参数、模式匹配和策略， 都是为了让书写更方便。解析与精化把这些写法变成核心声明，再由内核检查。 策略可以很复杂，可以搜索，可以调用 AI；在普通的证明路径上，它最后仍须交出 一个能被内核接受的项。策略报告成功，并不会给逻辑增加一条新规则。

到这里，我们已经遇到两种不同的数学。 一种是在系统内证明一个命题，例如某个函数是连续的。 另一种是研究系统本身：它的规则是否互相协调，是否会推出矛盾，检查算法是否符合规则。 后者就是元理论。Hales 所追问的，主要是这第二种数学。

只说“基于依赖类型论”还不够

Lean 的基础通常被称为归纳构造演算（CIC）的一种变体。 这告诉了我们它属于哪个家族，却还没有给出它的完整规则。 Lean 和 Rocq 都来自这个家族，但它们并不是同一个形式系统换了两套语法。 元理论证明必须处理那些具体差别。

依赖类型的核心构造是 \Pi x:A.\,B(x). 它表示返回类型随参数变化的函数。设 B(n) 是长度为 n 的向量的类型， 那么 f:\Pi n:\mathbb N.\,B(n) 接受自然数 n 后，返回的就必须是长度为 n 的向量。 函数应用的规则写成 \frac{\Gamma\vdash f:\Pi x:A.\,B(x)\qquad\Gamma\vdash a:A} {\Gamma\vdash f\,a:B(a)}. 普通函数类型 A\to B 是返回类型不随参数变化的情形；全称量词也使用这个构造。 变量、常量、函数抽象、应用和局部定义构成了基本项语言。 实际内核还有字面量、投影等表示，它们同样需要有明确的检查与计算规则。

类型本身也是项，因此还要回答：一个类型的类型是什么？Lean 的回答是宇宙层级： \mathrm{Prop}=\mathrm{Sort}\,0,\qquad \mathrm{Type}\,u=\mathrm{Sort}(u+1),\qquad \mathrm{Sort}\,u:\mathrm{Sort}(u+1). 这里没有一个以自己为类型的“所有类型的类型”。 Lean 的宇宙还具有非累积性：已经属于某层的类型，不会自动也属于更高的一层。 宇宙多态可以让一个声明在不同层级实例化，显式提升可以构造高层副本； 二者都不是在系统中加入累积规则。

函数类型所在的宇宙，体现了命题与数据的区别。 若 A:\mathrm{Sort}\,u，并且 x:A\vdash B(x):\mathrm{Sort}\,v，则 (\Pi x:A.\,B(x)):\mathrm{Sort}(\operatorname{imax}(u,v)), \qquad \operatorname{imax}(u,v)= \begin{cases} 0,&v=0,\\ \max(u,v),&v\gt 0. \end{cases} 如果值域是命题，量化后的结果仍然是命题，即使所量化的对象来自很大的宇宙。 这就是 Prop 的非直谓性。数据所在的宇宙遵循另一分支。

这些不是实现时随手选的记账方式，而是决定什么表达式能够成为类型的规则。 不过，选择非累积宇宙，只排除了一类由累积造成的多重类型归属； 它并没有自动证明整个系统的类型唯一性。这正是后面要回来的问题。

在 Lean 里，证明也参与了计算

类型检查不能只比较两个表达式的拼写。 如果 A 和 B 定义相等，一个类型为 A 的项就可以用于要求 B 的地方。 把抽象的定义相等写成 A\equiv B，它包含函数应用时的代入、定义展开、 局部定义的替换，以及递归器和商类型的计算规则。 例如，(\lambda x.\,x)\,a\equiv a。 函数和适用的结构类型还满足相应的 \eta 规则：把函数重新写成 \lambda x.\,f\,x，或者把结构拆成字段再组装回来，内核可以识别它们与原对象相同。

这里的相等，与命题 a=b 不同。 定义相等属于检查器使用的转换规则；命题等式则是系统中的一个类型，需要一个证明项。 函数外延性从逐点相等推出函数的命题等式，也不能与函数的 \eta 转换混为一谈。

Lean 还有一个很方便、也很重要的选择：同一命题的任意两个证明，都被视为定义相等。 这叫证明无关性。它并不把不同命题视为相同，也不会为未证明的命题提供证明。 它让数学对象携带的证明不必影响对象的身份：一个数满足某条件， 通常不会因为我们换了一种证明这个条件的办法，就成为另一个数。

与此相配的是消去限制。存在命题的证明，一般不能通过模式匹配就提取成可计算数据。 某些特殊形式允许从命题向数据消去，等式就是重要的一种： 沿着 h:a=b，可以把 B(a) 中的对象搬运到 B(b)。

Lean 还支持 K-like 归约。 对于相应的单构造子命题类型，若构造子没有参数以外的实参，而且索引满足转换条件， 递归器可以把主证明当作那个构造子处理，即使该证明没有显式展开成构造子。 在等式的情形，这涉及识别两个端点定义相等。 所以，一份 Lean 基础的说明不能只列出几条命名公理，还必须交代这样的计算规则。

这些规则也是 Lean 与 Rocq 的实质区别所在。 Rocq 的普通 Prop 不直接把任意两个证明放进同一个定义相等类； 它另有具有严格证明无关性的 SProp，配套的消去限制也不同。 把证明无关性作为命题公理加入，与把它作为转换规则加入，会产生不同的元理论问题。 仅仅说“它们都是 CIC”，不能省去这部分论证。

归纳类型，以及三条常用公理

自然数、列表、逻辑连接词、命题等式，都由归纳声明提供。 一个归纳声明不只是列几个构造子的名字：内核要检查类型、宇宙、参数、索引和严格正性， 再建立递归器及其计算规则。互归纳与嵌套归纳使这个过程比自然数的例子复杂得多。

自然数的归纳原则说，给出 P(0)，再给出从 P(n) 到 P(n+1) 的步骤， 就能对每个自然数得到 P(n)。 递归器把这个原则写成一个有类型的操作；计算规则还规定它在零和后继处分别怎样工作。 推广到带索引的归纳族，要把依赖关系一起带入构造。 因此，验证几个熟悉的例子，与证明完整归纳声明机制可靠，距离并不小。

Lean 也直接支持商类型：构造商、把代表元送入商、提升尊重关系的函数、作归纳， 以及在代表元上的计算，都有对应机制。 Quot.sound 进一步保证，满足给定关系的代表元会得到相等的商类。 它与下面两条一起，构成普通 Lean 数学最常见的标准公理集合。

公理 数学内容
propext 逻辑等价的命题相等：(P\leftrightarrow Q)\to P=Q。
Quot.sound 满足商关系的代表元给出相等的商类。
Classical.choice 从一个类型非空的证明得到该类型的一个元素。

排中律可以从标准基础导出，不需要再列作第四条独立公理； 函数外延性也可以通过商机制证明。 但使用者仍可声明额外公理，所以“Lean 只有三条公理”不能理解为系统不允许其他公理。

这也说明 #print axioms 能告诉我们什么。 它追踪的是对公理声明的依赖，不会打印整个逻辑基础。 即使结果显示不依赖任何公理，那个证明仍然依赖宇宙、转换、归纳类型和证明无关性等规则， 也依赖检查器正确执行这些规则。 Mathlib 则是在这套基础之上组织数学定义和定理的库；它不是另一种内核。

“基础已经证明”究竟指什么

读到一个系统已经“验证”，我更想接着知道：验证的宾语是什么？ 是某段程序符合规范，是抽象规则有一个模型，还是这些规则绝不可能推出矛盾？ 这几种结果之间有联系，却不能互相替代。

可靠性（soundness）把推导与解释联系起来： 凡是按规则推出的判断，在指定的语义中都成立。 一致性说的是，系统不能无前提地推出矛盾。 相对一致性 则在一个明确的外部假设下得到这个结论，例如假设存在适当的集合论模型。 其形式可以概括为 \operatorname{Con}(S)\Longrightarrow\operatorname{Con}(T). S 的假设是定理的一部分。 哥德尔第二不完备定理没有禁止这样的相对论证，也没有禁止证明一个程序符合给定规范。

这里的系统 T 必须固定准许的公理，并排除 sorry 等未完成证明的占位。 如果允许随意添加一个矛盾公理，就不可能对所有这样的环境作一致性保证。 同样，从局部假设 False 推出结论，只是在作条件推导，没有推翻系统的一致性。

类型保持 研究归约是否保留类型；合流性 研究从同一项走两条归约路径后，结果能否继续走到共同终点。 弱规范化要求存在到达规范形的路径，强规范化要求每条归约路径都终止。 每一个命题都要说明使用哪种归约关系、研究哪些项。

检查算法的完备性 又是另一件事：理论上成立的判断，算法是否全都能识别？ 可靠性只要求接受时没有误判。 一个不会接受错误证明的检查器，仍可能拒绝某个合法但难以处理的证明，或者耗尽资源。 后面几个容易令人不安的结果，正需要放在这个区别下理解。

那个看似显然的类型唯一性

Hales 提到的类型唯一性，听上去像是一句定义，实际上是需要证明的结论。 在固定环境和上下文中，类型唯一性要求 \Gamma\vdash t:A,\quad\Gamma\vdash t:B \quad\Longrightarrow\quad\Gamma\vdash A\equiv B. 这里的 t 是已经精化完成的同一个项，不是在不同上下文中可以被解释成不同对象的数字记号。

困难很快就会在函数应用 f\,a 上出现。 两份推导可能先把 f 赋予不同的函数类型；要比较最后得到的结果类型， 就需要从函数类型的相等恢复其组成部分的相等。 这类性质叫定义性反演。 其中，\Pi 单射性要求从 \Gamma\vdash(\Pi x:A.\,B)\equiv(\Pi x:A'.\,B') 推出定义域相等，以及值域在适当转换后的上下文中相等。 Sort 单射性要求宇宙相等蕴含层级等价； 还需要排除宇宙与 \Pi 类型之间的混淆。 这些都针对定义相等，不能把前提换成命题等式后仍当作同一条定理。

转换又包含证明无关性，而证明无关性的前提要知道两个项具有怎样的类型。 于是，证明类型唯一性要使用转换的结构性质，证明转换的结构性质又会遇到类型信息。 需要一个真正有效的归纳安排来打破这种相互依赖。

Mario Carneiro 的 2019 年论文曾试图通过分层判断完成这件事。 后来发现，代入步骤需要的层数上界是 \max(i,j)，实际能得到的却是 i+j， 原来的归纳论证因而不能成立。 Carneiro 在后续 Lean4Lean 论文中公开说明了错误，并将相关结论列为猜想。 发现的是证明缺口，没有同时发现这些结论的反例。

这不意味着已有基础工作都要推倒。 例如，弱化说明在正确调整变量引用后， 增加变量可以保持原判断；项代入、宇宙代入，以及“一个项的类型本身属于某个宇宙”， 都有可指认的形式化结果。 Lean4Lean 还证明了部分检查函数与抽象规范的关系。 这些结果带有各自的环境与上下文条件，不应被抹去，也不应被扩大成整个实现已经验证。

还要留意“抽象理论”究竟是哪一版。 Lean4Lean 使用带类型的判断 \Gamma\vdash s\equiv t:A，并把类型判断定义为它的对角情形； 2019 年论文则使用相互定义的类型判断和不标注类型的相等判断。 Lean4Lean 论文第三版把两种表述的等价性也列为猜想。 它对核心规则的论证还带有关于全局环境及扩展的条件，归纳扩展的部分规格仍待完成。 因此，读到某个核心定理已证，不能直接把覆盖范围扩张到现行内核接受的一切声明。

在本次核对的 Lean4Lean 修订 67f63b0 中，关键单射性引理仍含 sorry， 类型唯一性的证明依赖它们。 加强（strengthening）， 也就是满足无依赖条件时删去未用变量的性质，同样还有证明占位；它不是弱化的自动逆推。 另一个项目 lean4lean-model 在修订 27fb3b6 中， 也还没有完成其目标相对一致性定理。 这些都是关于具体公开版本的观察，不代表所有分支或所有研究者都没有进一步进展。

不终止，为什么不等于矛盾

另一些结果确实是负面的，但负面之处需要说准确。 Carneiro 的论文对其研究的演算给出了理想定义相等的不可判定性论证。 Andreas Abel 与 Thierry Coquand 则证明， 相关的非直谓、证明无关等式理论不满足规范化。

后一个结果甚至包含一个使用命题外延性的闭合证明项， 它没有弱头规范形， 即连只要求头部归约停止的形式都到不了。 但这个项证明的是一个真命题，并不是 False。 论文的具体 Lean 示例使用 3.4.2 版，后续 Lean4Lean 论文也讨论了这一障碍。 要求新递归定义通过终止性检查，并不等于已经证明类型论全部转换规则组合后的全局规范化。

我认为，这里最值得避免的误读，是把三个问题串成一条未经论证的因果链： “计算可能不停，所以相等不可判定，所以系统可能推出矛盾。” 非终止例子本身不是一般意义上的不可判定性证明；不可判定性又不等于不一致。 每一步都需要独立的论证。

这些结果真正限制的是某些证明方法。 我们不能随意假定，把所有表达式算到规范形之后再比较，就能完成所需的检查与元理论证明。 而实际算法的相等判定，也不能被当作理想转换关系的完整实现。 论文讨论了算法相等的非传递性，以及把这种算法关系放进类型判断后， 归约前被接受、归约后不再被同一算法型判断接受的情形。 这与抽象判断具有传递规则，是不同层次的陈述。

Hales 所提到的修正版 Church–Rosser 问题，也必须落实到具体的归约关系。 纯 \lambda 演算的合流定理，不能因为名字熟悉就拿来替代 Lean 所需的论证。

这些缺口正在怎样补

一条路线是继续完成语法元理论，再把检查器与它连接起来。 Carneiro、Coquand 和 Meven Lennon-Bertrand 在 AITP 2026 的报告中，讨论了单射性与类型唯一性的形式化。 摘要末段仍列出分层和传递步骤中的障碍；尝试包括增加分层信息， 或者把类型之间的等式与普通项之间的等式分开组织。 这是在修补证明结构，而不是因为题目里出现了“formalization”，就可以宣布整体完成。

另一条路线绕开“先规范化”。 2026 年论文《Definitional Inversion, Without Normalisation》使用 域模型，用有限信息近似项的行为。 逻辑关系 把这些语义信息与语法项联系起来，并与类型及项构造相容。 这样，证明可以恢复所需的类型形状，而不必先把每个类型完整地算完。 这项工作已有 Agda、Lean 和 Rocq 形式化，各自覆盖的扩展不同； 推广到完整归纳、余归纳细节以及与 K 结合的证明无关性，仍是论文明确留下的挑战。

这里的“模型”也不能一听就理解为一致性模型。 这种域模型容纳部分计算；论文从带 Type : Type 的玩具理论展开方法， 而那个理论已知不一致。 类型构造子的单射性可以是一项很有用的结果，同时并没有证明目标系统的一致性。

第三条路线直接通向集合论语义。 最初的图像很直观：把类型解释为集合，把项解释为集合中的元素； 假命题对应空集，真命题对应单元素集合，于是同一命题的证明在模型里只留下同一个点。 数据宇宙则必须有足够的封闭性，容纳函数空间和归纳构造。

Joachim Breitner 的 Con-Leche 就为一个实际检查器走了这条路。 其形式化主定理说，在规定的验证模式和集合论假设下，凡是它接受的声明环境，都有一个模型。 由于其中的 False 被解释为空集，就可以排除被接受的 False 定理声明。 项目报告已经检查过 Mathlib。这是实质性的成果，不应因为完整抽象元理论尚未完成而被忽略。

它的设计取舍也值得看清：为了使直接语义证明成立，检查器愿意多作一些类型比较。 它不必先把完整抽象系统的全部反演性质都证明出来，再沿那条路验证每个算法步骤。 因此，Con-Leche 的成功与 Lean4Lean 仍有未完成引理，可以同时成立。

集合模型为什么不能顺便证明 \Pi 单射性？ 看看普通的集合论函数空间就明白了：从空集到两个不同集合的函数集合， 都是只含空函数的单元素集合。 所以，两个解释相同，不意味着两个语法构造相同。 排除 False 的居民，与从定义相等恢复类型的组成部分，需要不同的论证。

Con-Leche 的模型接口假设一条 Grothendieck 宇宙链。 这里的宇宙是满足传递性、配对、幂集和相应索引并封闭条件的集合。 桥接工作从一列递增的不可达基数构造这个接口。 不可达基数是不可数的正则强极限基数： 正则性要求少于 \kappa 个小于 \kappa 的序数的上确界仍小于 \kappa； 强极限条件要求对每个基数 \lambda\lt \kappa 都有 2^\lambda\lt \kappa。 这是模型证明的外部假设，不是要求每个普通 Lean 定理都额外声明一条大基数公理。 桥接定理连接的是两套模型假设，也不会自动填掉 lean4lean-model 中另一个定理的占位。

Con-Leche 的实现与证明由 AI 在 Breitner 指导下完成，公开讲解也注明了 AI 协作。 这可以是研究进展，却不能被改述为已经完成独立人工审计。 检查算法的证明与编译器、运行时、输入输出驱动等环节的信任边界，仍须分别交代。

还有一条颇有启发性的路线：把隐式转换变成显式证明。 Rishikesh Vaishnav 的 Lean4Less 将证明转换到定义相等规则更少的理论中。 原来因 p,q:P 而直接把 T(p) 与 T(q) 视为同一类型的地方， 可以改为先给出 p=q，再得到 T(p)=T(q)，最后明确地搬运项。 相关强度由目标系统中的命题性证明无关原则承担，没有因为删除了转换规则就凭空消失。

这有助于向其他系统导出证明，也有助于研究更小的核心。 但要由此得到源系统的一致性，还需要相应的翻译正确性和目标系统的一致性。 论文报告了特定库的翻译结果，当前仓库也列出兼容性与翻译限制； 它没有宣布完成现行 Lean 全部基础的相对一致性证明。

截至现在，走到了哪一步

把这些工作放在一起，已经不适合用“证明了”或“没有证明”两个格子来装下全部信息。 更准确的账目如下，日期仍是 2026 年 10 月 19 日。

问题 已有证据与尚存边界
核心结构引理 Lean4Lean 已有弱化、代入、类型合法性等结果，须保留其环境条件。
类型唯一性与定义性反演 核对的主线修订仍有缺口；域论工作已证明指定理论及扩展中的结果。
加强 核对的逆向弱化结果仍留有证明占位。
完整抽象目标的相对一致性 lean4lean-model 的指定目标尚未完成；模型路线与检查器专属成果应另列。
Con-Leche 的接受结果 已有形式化模型定理，限于规定模式与模型假设；并非官方 C++ 内核的验证。
规范化与理想转换 已有负面数学结果，各有范围；它们不等于不一致。
完整执行链 检查算法的定理不会自动覆盖编译器、运行时、输入输出和硬件。

Hales 与研究者之间需要认真对待的分歧，也在这里。 关于绕开类型唯一性的模型路线，可以有相当强的数学信心； Hales 要求的则是覆盖明确、公开完整、能够审查的论证。 一条可信的路线说明与一份完成的证明之间，还有工作需要做。

软件漏洞是另一项不能省略的事实。 Leonardo de Moura 的 2026 年 8 月复盘记录了内核与运行时错误， 以及 Lean 4.33.1 中发布的修复。 这些错误曾让程序接受错误的证明，说明实际实现需要核查； 它们本身并不把抽象逻辑的某条规则变成了矛盾。 修复实现与完成元理论，是互相补充的两项工作。

Elan、Lake 在这件事里做什么

谈到“另一个内核”时，很多人会把它与 Lean 的版本、Lake、Elan 或 Mathlib 混在一起。 这些名字其实处在不同的位置。

工具链是一套安装好的 Lean 及配套程序和库。 Elan 管理和选择工具链，通常根据项目的 lean-toolchain 文件决定使用哪个版本。 Lake 读取项目配置、解析依赖、安排构建目标；lake-manifest.json 记录解析后的依赖版本。 只固定 Lean 版本，还没有固定全部数学库；只固定依赖，也没有说明实际运行了哪套工具链。

在这个环境里，Lean 的前端产生核心声明，内核检查它们。 编译器与运行时负责执行程序，其中包括工具本身的大量实现。 Mathlib 提供数学内容；编辑器则把这些工具的结果呈现出来。 Elan、Lake 和编辑器都不因此成为另一套逻辑。

从工具链到证明复核
  1. Elan 选择工具链
  2. Lake 组织项目构建
  3. Lean 解析与精化
  4. 官方内核检查声明
  5. 导出声明
  6. 外部检查器重新检查声明

这个流程说明各工具怎样衔接，并不代替各阶段正确性的证明。 .olean 是构建时保存的模块产物；导出格式则把声明提供给其他检查器。 二者的兼容性都与版本有关。 lake env 为一个命令设置项目环境，也不等于证明该命令的实现正确。

为什么会有这么多内核

外部检查器检查核心声明，不必同时实现编辑器、策略语言、包管理器和编译器。 官方前端生成的证明，可以导出后交给另一套程序复核。 这与把整个 Lean 项目移植到另一种语言，或者把 Lean 3 项目升级到 Lean 4，是不同的任务。

实现或工具 与其他实现的关系
官方 Lean 4 内核 日常 Lean 系统使用的 C++ 检查器，以及它依赖的运行时。
lean4checker 把保存的声明重新交给官方内核；重复检查，但没有换掉内核算法。
Lean4Lean 从官方 C++ 算法出发，用 Lean 实现检查器，并建立抽象规格和验证；共同设计也可能带来共同缺陷。
Nanoda Rust 实现的外部检查器；不同实现有利于复核，但不因此自动得到一致性定理。
Con-Leche 用 Lean 实现，增加适合直接模型证明的检查步骤，具有针对自身接受行为的形式化保证。
Con-Ron Con-Leche 的 Rust 移植，改变数据表示，并通过中间 Lean 模型及 Aeneas 对 Rust 的翻译建立模拟关系；翻译与驱动假设仍须计入。

Lean4Lean 自己就说明，它不是完全独立的净室重写。 Con-Ron 希望减少对 Lean 执行环境的共同依赖，也明确说明证明没有覆盖哪些环节。 多套检查器一致接受是一项有价值的证据，但不能把它们的所有假设都当成彼此独立。 Kernel Arena 为这些实现提供共同测试与比较；它是一项工程设施，不是一份元理论证明。

反过来，一个检查器拒绝某份输入，也需要分辨原因：声明有错、特性尚不支持， 还是资源耗尽？不同版本未必接受相同的导出格式与扩展。 Lean 3 与 Lean 4 更是系统的不同代际；嵌套归纳、结构的 \eta 等变化， 都使旧的基础论证不能不加说明地覆盖新的系统。

接着 Hales 的问题往前走

这些区分最终会改变我们怎样读一句“已经通过 Lean 验证”。 lake build 组织构建；lean4checker 可以重新检查保存的声明； 当前的 lake check 组织构建、导出、复核和公理检查， –paranoid 还要求随工具链分发的外部检查器都接受。 Lake 在调用这些程序，并没有自己变成它们的内核。

操作条件也要算在保证的范围里。 文档中的项目检查沙箱依赖 Linux；用 –from-export 检查一份现成导出， 只能说明那份导出被接受，不能自动建立它与任意源项目的对应。 这些条件并不削弱一个准确陈述的结论，反而让结论可以被别人复核。

还有一个任何内核都不能替数学家回答的问题：形式陈述是不是原来想证明的命题？ 假设可能被加强，结论可能被削弱，一个符号也可能指向意料之外的定义。 正确检查另一道题的证明，不会自动回答原来的问题。 所以，可靠的形式化结果始终需要对陈述、定义和假设的理解。

我赞同 Hales 对完整、公开、可理解的基础论证的要求。 数学界不应满足于听到“内核很小”，就把有关推导规则和实现的困难一笔带过。 但已有的结构定理、直接模型证明、多实现复核和证明翻译，也都应当得到准确的位置。 尤其不能把“某条证明路线还没有走完”，改述为“Lean 已经被发现逻辑矛盾”。

一份真正有用的验证说明，应当让读者知道：证明的是什么，依赖哪些定义与公理， 由哪个版本、哪个模式的检查器接受，引用的基础定理又覆盖了哪一部分。 这些信息一旦展开，讨论就能离开笼统的放心或担心，回到可以继续推进的数学问题。

参考资料

以下是本文的主要来源，研究状态核对至 2026 年 10 月 19 日。 论文中的定理、仓库中的目标定理，以及一个库通过检查，是不同种类的证据。 本次工作查阅这些资料，不声称重新构建或独立审计了其全部形式化证明。

论文与研究报告

规格、实现与核对版本