Lean形式化

1 引言

本栏目面向计量经济学教师与研究者，系统介绍 Lean 形式化证明：它与课堂 LaTeX 推导有何不同，底层逻辑是什么，用哪些工具，怎样实施，以及如何解读 lake build（Lake 构建，Lean 的编译/检查命令）的结果。

形式化教程写在本仓库 block-lean/，与章节复现、矩阵预备并列。当前交付是可读讲义，不是 Lean 子工程：这里没有 lakefile.toml，也不把 Mathlib（Lean 的数学库）拷进站点。方法页仍见 实证复现与 Lean 考证；教材原文在姊妹仓库 hansenEM。

建议阅读顺序：

1. 课堂证明与形式化证明：先对准认知差异。
2. 交互式定理证明简史 与 类型论与内核：弄清「机器在检查什么」。
3. 技术栈 与 工作流：准备动手。
4. 如何解读形式化结果：避免把编译通过说成「证明了教材原句」。
5. 计量经济学路径 与 学习资源：接到 Hansen 与练习。