课堂证明与形式化证明

计量教师面对的范式转换

计量课上我们习惯用 LaTeX 写「证明」。那是给人读的论证：省略显然步骤、依赖共享记号、允许读者用直觉补全。Lean 形式化是给内核读的论证：每一步必须是类型正确的项，或能被策略展开成这样的项。两者都叫证明，对象、标准和失败方式都不同。

本页把差异说清楚，并接到本仓库已有的 L1 / L2 / L3 分层（教学展开 / 计算核对 / 逻辑证书）。后续各篇分别讲历史、逻辑、工具与计量落地。方法总页见 实证复现与 Lean 考证。

1 我们原本在做什么

中高级计量课的典型理论环节是：

  1. 在黑板上或讲义里陈述定理（无偏性、Frisch–Waugh–Lovell（FWL）定理、一致性……）。
  2. 用 \(\LaTeX\) 展开代数：正规方程、投影幂等、条件期望塔性质。
  3. 用「于是」「显然」「由正则条件」跳过测度论或极限交换。
  4. 用习题让学生复述同一条链。

这套做法的优点很具体：可读、可改、能和图、表、模拟放在同一份讲义里。本仓库的默认理论交付仍是这一层，即 L1 教学展开。

它的限度同样具体。印刷证明检查的是说服力，不是完备性。读者是否接受「显然」，取决于训练，不取决于机器。教材压缩证明时，省略的往往正是学生卡住的地方；有时印刷陈述本身过强或有误，课堂推导会把错误一起写顺。

2 形式化在检查什么

交互式定理证明（ITP, interactive theorem proving）把「定理 + 证明」写成一种程序。Lean 的逻辑是依赖类型论（dependent type theory）：命题是类型，证明是该类型的项。若内核接受 t : P，则在该系统的公理下，\(P\) 已被推出。这是 Theorem Proving in Lean 4 开篇的标准表述 (Avigad 等 2025年)。

因此形式化改变的不是「要不要写数学」，而是：

维度 课堂 / LaTeX Lean
读者 人；可容忍省略 内核；不容忍未声明步骤
证明是什么 叙事与计算的混合文本 类型正确的项（或生成该项的策略脚本）
「显然」 社会约定 必须变成引理、库定理或策略
反馈时间 批改、讨论、自己复查 光标处即时目标状态
失败 论证不令人信服 类型错误、未关闭目标、sorry
信任根 作者与同行 小内核 + 显式公理表
与原文关系 通常默认「就是书上那条」 必须单独论证陈述是否同义

Mathematics in Lean 把这一点说成一场游戏：对象有类型，命题的类型是 Prop，证明是类型为该命题的表达式；写出 sorry 是作弊，系统知道 (Avigad 和 Massot 2025年)。

3 三种证书，不要混用

本项目把「证明」拆成三层，避免用文采或数值模拟冒充逻辑证书。

flowchart TB
  latex["L1 教学展开<br/>Quarto + LaTeX"] --> calc["L2 计算核对<br/>R / 矩阵恒等式"]
  latex -.-> lean["L3 逻辑证书<br/>Lean + Mathlib"]
  latex -->|"说服人"| reader["课堂读者"]
  lean -->|"检查项"| kernel["Lean 内核"]

  • L1：补中间步、列假设、拆引理。写在 .qmd。这是教师最熟的工作，也是形式化之前几乎总要先做的一步。
  • L2：能算的才算。例如核验 \(P=P^2\)、\(M=I-P\)，或有限样本模拟。这是计算证书。
  • L3：lake build 通过、且目标定理不依赖 sorry。这是逻辑证书。它只保证这个形式陈述可从给定公理推出。

未做 L3 时，不要写「已形式化证明」。L1 写得很细，也仍然是给人读的。

4 认知上真正别扭的地方

对已会写证明的教师，转换成本通常不在「数学太难」，而在下列习惯：

1. 目标是一等公民。
课堂证明是线性叙述。Lean 策略证明是在一个目标栈上操作：当前要证什么、上下文有哪些假设，Infoview（信息视窗，显示当前证明目标）随时显示。Massot 指出，这种「战术状态」在黑板上几乎无法持续模仿，却是学生学习逻辑结构时最有用的反馈 (Massot 2024年)。

2. 「显然」必须被点名。
\(X'X\) 可逆、条件期望几乎处处定义、积分与极限可交换，在讲义里常一笔带过。在 Lean 里它们是假设、引理或 Mathlib 定理。形式化会把教材的隐含前提摊开——这正是它对教学有价值的原因，也是进度变慢的原因。

3. 定义先于推导。
LaTeX 里可以先写公式再补「其中 \(P\) 为投影」。Lean 里未定义的名字无法通过精化。计量里大量冲突来自同一记号：\(E(Y\mid X)\) 是条件期望还是线性投影？\(X'X\) 奇异时估计量取什么值？这些必须在写 theorem 之前决定。

4. 库比记忆更权威。
课堂证明调用「条件期望的塔性质」。Lean 调用 Mathlib（Lean 的数学库）里带精确类型的 condExp 引理。你要先学会找定理，而不是从零复述测度论。这更像查手册写程序，不像默写板书。

5. 语法错误会盖过数学错误。
Iannone、Marasingha 与 Thoma 在《美国数学会通告》（AMS Notices）中总结课堂经验：学生要把「学证明」和「学一门不容错的语言」叠在一起；对不上括号的报错，看起来不像数学 (Iannone 等 2025年)。教师自己也会经历同一阶段。这不说明形式化无用，只说明入门必须单独安排时间，不能指望「在计量课边上顺便学 Lean」。

6. 技能迁移不是自动的。
把策略脚本译回纸笔证明，需要刻意练习。Verbose Lean 一类受控自然语言，正是为了缩小「程序外观」与「纸面证明」的距离 (Massot 2024年)。计量评注的策略是反过来：L1 保持纸面可读，L3 另开工程，中间用 inventory（定理清单）对齐编号。

5 一个最小对照

课堂上一句话：若 \(n\) 为偶数，则 \(mn\) 为偶数。

Lean 可以写成证明项，也可以写成策略。Mathematics in Lean 的策略版大意是：引入 \(m,n\) 与「\(n=2k\)」，指定见证 \(mk\)，改写后再用 ring (Avigad 和 Massot 2025年)。读者不必在本页编译这段代码；应体会三件事：

  1. 假设被逐条引入，而不是写在段落里。
  2. 「偶数」被打开成存在量词，而不是口头定义。
  3. ring 替代了「整理一下即得」——自动化仍然产出可检查的项。

同一事实用 R 检查若干整数，只是 L2。类型检查通过，才进入 L3 的门槛。

6 对计量教学意味着什么

形式化不是要取代 Hansen 讲义或本仓库的 L1。更准确的分工是：

  • 课上仍用 LaTeX 讲结构、动机与「为什么这条定理重要」。
  • L1 笔记把压缩证明展开到学生能逐步核验。
  • 若某条定理值得钉死（例如 FWL、塔性质、普通最小二乘（OLS, Ordinary Least Squares）无偏性），再把它做成 inventory，并在将来的 L3 工程里给一个可编译陈述。
  • 形式化过程中发现的「印刷陈述过强 / 需几乎处处 / 需满秩」，必须写回 L1，而不是只存在于 .lean 文件。

Avigad 等人把入门课里的 Lean 定位为：用形式对应物巩固推理模式，而不是把课上成证明助手课 (Avigad 2018年)。本栏目采取同一态度。目标读者已会写证明；缺的是把「证明」看成可检查伪代码的那一层概念。

7 本栏目的边界

  • 做：讲原理、历史、工具、工作流、如何读结果；为 Hansen 形式化准备概念与对照方法。
  • 暂不做：在本仓库初始化 Lean 工程、把 Mathlib 源码拷进仓库（vendor）、声称某条 Hansen 定理「已形式化」。
  • 对照：社区项目 lean-hansen-econometrics 与 OpenAI 的 Navier–Stokes Lean 证书，都是方法参照，不是本站产物。

下一篇从 AUTOMATH 讲到 Lean 4 与 Mathlib，说明这套工具从哪来。

参考文献

Avigad, Jeremy. 2018年. Learning Logic and Proof with an Interactive Theorem Prover. https://www.contrib.andrew.cmu.edu/~avigad/Papers/learning_logic_and_proof.pdf.
Avigad, Jeremy, 和 Patrick Massot. 2025年. Mathematics in Lean. https://leanprover-community.github.io/mathematics_in_lean/.
Avigad, Jeremy, Leonardo de Moura, Soonho Kong, 和 Sebastian Ullrich. 2025年. Theorem Proving in Lean 4. https://leanprover.github.io/theorem_proving_in_lean4/.
Iannone, Paola, Gihan Marasingha, 和 Athina Thoma. 2025年. 《Teaching Mathematics with Lean: Interactive Theorem Provers in the Classroom》. Notices of the American Mathematical Society 72 (7): 740～47. https://doi.org/10.1090/noti3184.
Massot, Patrick. 2024年. 《Teaching Mathematics Using Lean and Controlled Natural Language》. 15th International Conference on Interactive Theorem Proving (ITP 2024). https://doi.org/10.4230/LIPIcs.ITP.2024.27.