类型论与内核
Lean 在检查什么
不理解类型论，也可以用 Lean 做题——社区明确说过，用 Mathlib（Lean 的数学库）并不要求先读完同伦类型论（HoTT, Homotopy Type Theory） (Lean prover community 2025年)。但作为要判断「这段形式化算不算证明了 Hansen 定理」的教师，需要一张比语法更小的地图：项、类型、命题、证明、内核、公理。本页只画这张地图。语言细节以 Theorem Proving in Lean 4 为准 (Avigad 等 2025年)。
1 每个表达式都有类型
Lean 的基础是依赖类型论（dependent type theory）的一个变体，常被说成「带归纳类型的构造演算」（即归纳构造演算 CIC, Calculus of Inductive Constructions 的近亲）。要点不是术语，而是三条判断：
e : T读作「表达式e具有类型T」。- 类型本身也是表达式，所以有
T : Type或P : Prop。 - 检查证明 = 检查某个项是否具有某个命题类型。
Mathematics in Lean 用三个 #check 例子把世界分成三类 (Avigad 和 Massot 2025年)：
- 对象：
2 + 2的类型是ℕ；fun x => x + 3的类型是ℕ → ℕ。 - 命题：
2 + 2 = 4的类型是Prop。 - 证明：若
easy : 2 + 2 = 4，则easy是该等式的一个证明。
课堂语言里「设 \(X\) 为 \(n\times k\) 矩阵」对应「X 具有某个矩阵类型」；「定理 \(P\)」对应「我们要构造类型为 P 的项」。
2 Curry–Howard：命题即类型
自然演绎里，蕴含 \(P\to Q\) 的引入规则是「假设 \(P\)，推出 \(Q\)」；函数类型 P → Q 的引入规则是 λ 抽象。两者同构。这就是 Curry–Howard 对应（命题即类型、证明即程序），口号是 propositions as types, proofs as programs。
Lean 把命题类型 Prop 与普通数据的 Type 放在同一宇宙层级的底部（Prop 即 Sort 0），并让蕴含直接使用函数箭头 (Avigad 等 2025年)。一张对照表足够上课用：
| 逻辑 | Lean 类型 | 证明/程序 |
|---|---|---|
| 命题 \(P\) | P : Prop |
项 t : P |
| 蕴含 \(P\to Q\) | P → Q |
函数：把 P 的证明送到 Q 的证明 |
| 合取 \(P\land Q\) | P ∧ Q |
序对 |
| 析取 \(P\lor Q\) | P ∨ Q |
带标记的并 |
| 全称 \(\forall x, P(x)\) | (x : α) → P x |
依赖函数 |
| 存在 \(\exists x, P(x)\) | ∃ x, P x |
见证 + 性质证明 |
| 真 / 假 | True / False |
单元 / 无引入 |
对计量教师，这意味着：写证明很像写函数。引入假设像给函数加参数；用已有引理像调用函数；把目标拆成引理像把大函数拆成小函数。Iannone 等强调，这种分解正是学生在纸面证明里也该学的技能 (Iannone 等 2025年)。
3 Prop 的特殊性
Lean 的 Prop 是证明无关的：同一命题的两个证明在定义相等的意义上不可区分。设计意图是：证明不参与计算，抽取程序时可擦掉 (Avigad 等 2025年)。
后果有两条，计量里都会碰到：
- 你通常不关心「哪一个」无偏性证明被选中，只关心无偏性成立。
- 等式
s = t也住在Prop里。用等式改写表达式时，系统在做类型上的转换；这可以阻碍内核约化，但不妨碍虚拟机在擦除命题后求值。
Type 里的对象（矩阵、随机元的具体函数）是数据；Prop 里的定理是证书。把估计量本身和「它无偏」混成一个定义，会让类型变得难用——Hansen 形式化项目因此把估计量的全函数化（奇异时怎么办）与定理的假设（可逆时无偏）分开，见 计量路径。
4 项风格与策略风格
构造证明项有两条路，可以混用 (Avigad 和 Massot 2025年)。
项风格直接写 λ、have、show，像函数定义。它接近逻辑推导树，短证明很清晰，长证明难维护。
策略风格在 by 块里发指令：intro、apply、rw、exact、simp。策略（tactic）是生成项的程序；内核检查的仍是项，不是策略文本。Infoview（信息视窗）显示当前目标，这才使交互成为可能。
-- 项风格（示意）
theorem and_comm_term (p q : Prop) : p ∧ q → q ∧ p :=
fun h => And.intro h.right h.left
-- 策略风格（示意）
theorem and_comm_tac (p q : Prop) : p ∧ q → q ∧ p := by
intro h
exact And.intro h.right h.left本页不编译这些片段。应记住：策略失败时，往往仍有一个未关闭的目标；用 sorry 可以暂时关闭它，同时向系统承认缺口。
5 归纳类型：对象从哪来
自然数、列表、命题连接词，在 Lean 里多半是归纳类型：给出构造子，再得到递归与归纳原理。这对应课堂上的「由生成规则定义，再用归纳法证明」。
Natural Number Game（NNG，自然数游戏）把这一点做成闯关：从 Peano 式公理出发证明 2+2=4 与交换律，逼你把「归纳」写成策略，而不是口头说「对 \(n\) 归纳」(Buzzard 和 Eugster 2025年)。计量用到的矩阵与测度空间，则已经由 Mathlib 定义为更复杂的结构；你很少从零写归纳，但「定义给出消去规则」这一思维仍然适用。
6 内核：信任根有多小
LCF（Logic for Computable Functions，可计算函数逻辑）传统的核心承诺是：只有内核能制造定理。策略、化简器、ring、外部计算，都必须最终还原为内核规则，或显式引入公理。
Lean 4 的内核实现类型检查与定义相等。用户代码、Mathlib、你的 Hansen 包装层，都不在信任根里。因此：
lake build通过，表示当前项目的导出声明通过了类型检查。- 它不自动表示「与 Hansen 印刷原句同义」。
- 它也不表示证明可计算；经典公理会破坏计算解释。
独立再实现一个类型检查器（外部 checker）是更强的审计，OpenAI 的 Navier–Stokes（NS，纳维–斯托克斯）仓库用 Comparator（对照检查器）走第二通道。计量侧更便宜的第二通道是：对照 hansenEM 原文审假设，见 结果解释。
7 公理：经典数学从哪进来
无额外公理时，Lean 的类型论偏构造性。数学库广泛使用三条（及由它们推出的排中律等）：
| 公理 | 直观 | 计量里何时出现 |
|---|---|---|
propext（proposition extensionality，命题外延） |
等价的命题相等 | 重写命题、集合外延的亲戚 |
Quot.sound（quotient soundness，商类型可靠性） |
商类型：相关则相等 | 几乎处处商、函数空间商 |
Classical.choice（选择公理） |
非空类型能挑出一个元素 | 存在性翻译成「选出估计量 / 选出极限点」 |
Diaconescu 定理：选择 + propext + 函数外延 ⇒ 排中律。因此 Mathlib 里的分析与概率，默认是经典数学，不是构造主义教材。#print axioms my_thm 列出依赖；若出现 sorryAx，则该定理尚未真正证明 (Avigad 等 2025年)。
对教师的实用规则：
- 看到
Classical.choice/propext/Quot.sound：正常，与「用了排中律的分析证明」同类。 - 看到
sorryAx：尚未证明。 - 看到
Lean.ofReduceBool或native_decide相关公理：信任根扩到了编译器求值，审计时要单独记一笔。
Mario Carneiro 的论文精确描述 Lean 3 时代的类型论；Lean 4 内核细节以官方 Type Checking in Lean 4 与参考手册为准 (Carneiro 2019年; Lean prover community 2025年)。入门不必读这些；要写外部检查器或争论「Lean 算哪套集合论」时才需要。
8 和集合论教材如何对接
计量研究生的实分析课通常从 ZFC（Zermelo–Fraenkel set theory with Choice，带选择公理的策梅洛–弗兰克尔集合论）讲。Lean 并不「先建 ZFC 再在里面做分析」；它在类型里直接定义实数、测度与积分，集合是 α → Prop 的包装。这足够表达几乎所有常规定理 (Avigad 等 2025年)。
翻译时常见摩擦：
- 几乎处处：教材写 \(E(Y\mid X)=X\beta\)，Lean 往往写
=ᵐ[μ]。 - 条件期望是 \(L^1\) 类还是函数：Mathlib 两者都有，教材默认函数。
- 「对所有 \(X\)」：类型论里要先定 \(X\) 的类型（矩阵、随机元、可测函数）。
这些不是内核的问题，是陈述工程的问题。工作流篇会把它当成实施步骤，而不是逻辑缺陷。