Lean 4 作为新一代交互式定理证明器与函数式编程语言，其内核架构融合了 Coq、CIC 与 Martin-Löf 依赖类型理论的精髓，同时通过自举编译和元编程框架实现了前所未有的可扩展性。本文从工程实现角度，深入剖析 Lean 4 内核的依赖类型理论实现、战术证明引擎与 AI 验证系统的设计要点。
内核架构的三层分离设计
Lean 4 的内核架构遵循严格的分层原则，将可信根（trusted base）最小化，同时为上层提供丰富的编程接口。这种设计使得开发者可以在不威胁系统可靠性的前提下，对 elaborator、战术和编译器进行激进的实验。
前端与 elaborator 层负责解析 Lean 语法、解决重载与记号问题、推断隐式参数与宇宙层级、执行类型类与强制转换搜索，最终生成完全显式的核心项。该层输出的是一种小型依赖 λ 演算，包含 Π/Σ、归纳类型、宇宙层级和常量定义。
内核层实现了逻辑核心，负责判定类型归属与定义相等性。内核只看到显式的核心语言，无法感知高层语法糖、宏或战术。这一层是系统唯一的可信基，任何定理或程序最终都会被归约为一个内核判断：如果通过类型检查则被接受，否则被拒绝。
运行时 / 编译器层将 Lean 作为通用编程语言执行，生成原生代码、中间表示或引用计数代码。从逻辑角度看，这部分位于可信核心之外，内核仅负责类型检查与归约。
核心依赖类型理论实现
Lean 4 内核实现的依赖类型理论接近 CIC（归纳构造演算），扩展了 mathlib4 和通用编程所需的功能特性。
宇宙层级系统采用层级结构 Sort u，其中 u, v 等层级代表 Type u 和 Prop 这类特定的排序。层级操作包括 max 与 imax，用于处理宇宙多态性和类型构造（如 α → β 或 α × β）中的层级组合。层级具有累积性：当 u ≤ v 时，Sort u 的项也可栖息于 Sort v。
** 依赖函数类型（Π-types）** 支持形式为 Π (x : A), B x 的一般函数，具有 β- 和 η- 规则。当陪域为命题时，这对应着蕴含与全称量化。** 依赖对类型（Σ-types）** 以 Σ (x : A), B x 形式支持带有投影与 β- 规则的依赖对，用于将数据与证明打包在一起，并支持构造性的存在性证明。
归纳类型与族涵盖一般归纳类型（包括索引族），内核自动生成对应的递归子 / 消除子原则，并强制执行正性与宇宙层级约束。这覆盖了常见数据类型（Nat、List、Bool、树结构等）以及数学与编程语言理论中使用的大型族。
命题与数据的区分通过单独的 Prop 排序实现，典型配置下 Prop 是证明无关的，而 Type u 用于数据类型。这种设计在支持命题即类型观点的同时，仍在内核层面保留了证明无关性。
判断形式与定义相等性
内核实现两种主要的判断形式：类型归属 Γ ⊢ t : T 表示项 t 在上下文 Γ 中具有类型 T；定义相等性 Γ ⊢ t ≡ u 表示两个项在可归约性与可定义常量的展开意义下相等。
定义相等性的判定通过归约完成：β- 归约处理 λ- 抽象，δ- 归约处理透明常量，ι- 归约处理模式匹配与归纳消除子，还包括部分 η- 规则（如函数）。类型检查依赖于检查推断类型与期望类型是否定义相等。
战术引擎的元编程框架
Lean 4 的战术引擎实现为一种带类型的证明状态变换器，位于通用元编程框架内。这种设计使得高效证明自动化可以在 Lean 本身而非外部语言（如 C++）中实现。
元编程框架包含四个主要 monad 层次：Kernel API 提供底层类型理论与表达式操作；MetaM 用于操作表达式与元变量；TermElabM 负责项的 elaborate；TacticM 在顶层处理战术状态。每个战术具有类型 TacticM Unit，它变换当前状态 —— 包含待解决的元变量列表 —— 最终必须解决所有目标才能关闭证明。
引擎暴露的核心原语操作包括：getMainGoal 与 getGoals 访问当前目标；setGoals 与 replaceMainGoal 更新活动目标；元变量创建与赋值。所有操作最终都经过内核验证。高层战术如 apply、intro[s]、simp 等使用这些原语加上 MetaM 操作（统一化、类型类搜索、规范化）实现。
可信基与公理扩展
Lean 的设计哲学是将可信逻辑核心保持最小化，尽可能将内容定义为可计算常量和库。经典数学原则（如选择公理或函数外延公理）作为非可计算的常量实现，声明类型但无计算内容。这些公理扩展了逻辑但不改变内核的归约规则，内核强制要求任何使用都必须通过类型显式声明。
形式化验证与自展
Lean4Lean 项目正在将 Lean 的类型理论形式化，并在 Lean 内部验证内核实现的正确性。该项目旨在证明内核正确实现了形式规则，从而排除实现错误导致的不一致性。这一工作朝向完全自展、自验证的内核迈进。
Lean 4 通过三层架构将依赖类型理论的数学严谨性与现代编译器的工程效率结合，在保持可信核心极小的同时，为定理证明与程序验证提供了强大的可扩展平台。
资料来源：本文核心事实参考 Lean 4 官方论文与文档、Metaprogramming in Lean 4 教程及 Lean 4 社区相关技术分析。