什么是 内核？

内核是实现 Lean 逻辑的软件；也就是能够构造 Lean 逻辑语言中的对象、并验证这些对象的正确性的最小化机制程序。主要组成部分：

• 一系列 名字 （name），用于寻址。
• 一系列 宇宙层级 （universe level）。
• 一系列 表达式 （expression）（λ-抽象、变量等）。
• 一系列 声明 （declaration）（公理、定义、定理、归纳类型等）。
• 环境 （environment）：名字到声明的映射。
• 表达式操作功能，例如绑定变量替换、宇宙参数替换。
• 类型检查核心操作：类型推断、化简、判定定义等价。
• 归纳类型相关的操作与检验：生成类型的递归器（消除规则），以及检查构造子的定义是否与类型规范一致。
• 可选的内核扩展，使上述操作能够直接处理 nat 与 string 字面量。

之所以要隔离出一个小型内核，并要求 Lean 中的定义被翻译成一种最简内核语言，目的在于提高证明系统的可信度。Lean 的设计允许使用者在功能完备的证明助理中工作，享受强大的元编程、丰富的编辑器支持和可扩展语法；同时又能把构造出的证明项导出为一种形式，使人们无需信任那些实现高级特性的代码，也能独立验证其正确性——这些高级特性正是 Lean（作为证明助理）高效且易用的原因。

在 Certified Programming with Dependent Types 一书第 1.2.3 节中，Adam Chlipala 提出了通常称为 **de Bruijn 准则（de Bruijn criterion）**或 de Bruijn 原则的概念：

当证明助理即便采用复杂且可扩展的策略来搜索证明，也会输出可在小型内核语言中表达的证明项时，就满足了 “de Bruijn 准则”。这些核心语言的特性复杂度大致与形式化数学基础（如 ZF 集合论）的提案相当。要相信一个证明，我们可以无视搜索过程中的潜在错误，只依赖一个（相对较小的）证明检查内核来验证搜索结果。

Lean 的内核足够小，小到开发者可以自行实现，并借助 导出器（exporter）¹ 独立检查 Lean 中的证明。Lean 的导出格式为每个声明提供了充分信息，使得用户可以选择只实现完整内核的一部分。例如，若只对类型推断、化简和定义等价的核心功能感兴趣，就可以省略归纳类型规范检查的实现。

除了上面列出的项目，外部类型检查器还需要一个针对 Lean 导出格式 的解析器以及一个美观打印器，分别用于输入和输出。解析器与打印器并不属于内核，但若想与内核进行有意义的交互，它们就不可或缺。