Lean 4——计算、类型与证明焊接在一起之处

上级：logic

Lean 4 是一个依赖类型的函数式语言，同时也是一个交互式定理证明器——这整条分支汇聚而成的实作综合体。

基础

归纳构造演算（Calculus of Inductive Constructions，CIC）：依赖类型论 + 归纳类型（定义 ℕ、列表、树，以及命题本身） + 一个宇宙层级（Prop 表示证明无关的命题；Type u 表示数据）。这套基础足够丰富，一个类型可以就是任何一条数学陈述。

证明即项；检验即类型检验

由柯里–霍华德对应可知，P 的一个证明就是一个类型为 P 的项。一个小小的可信内核对该项做类型检验——这就是德布鲁因判据（de Bruijn criterion）：你只需信任一个微小的检验器，而不必信任整个系统。在实践中，证明检验就是类型检验。

战术（tactic）——人与机器之间的桥梁

你很少手写证明项。你运行的是战术（intro、apply、simp、ring、omega……），它们在幕后构造出证明项。Lean 4 是自举的：它的战术／元编程语言本身就是 Lean，用户在证明器内部扩展证明器。这在人类式的推理与底层经归约的项之间架起了一座桥。

mathlib——大规模的形式化数学

一个由社区构建的庞大库——分析、代数、拓扑、数论——全部经过机器检验。它是"数学可以被完全形式化"这一论断的经验证明，也是可验证研究的基底（例如检验一个高难度证明是否存在漏洞）。

综合

Lean 既是一门真实、快速的编程语言，又是一个证明器，因此已验证的程序与其证明活在同一个对象里——程序＝证明，字面意义上的。三条线索在此汇合：

• 计算（turing-machines、lambda-calculus）——Lean 运行的部分；
• 类型（type-theory）——Lean 的基础；
• 证明（proof-theory）——Lean 通过归约来检验。

你写下的证明由机器通过类型检验来验证，而且你还可以对它们做计算。