实施方法与工作流

从教材定理到可检查的 Lean 声明

形式化不是从空文件里「把证明用 Lean 再打一遍」。可重复的做法是：先钉陈述，再搭骨架，再填内核可接受的项。社区 Hansen 项目把这一流程写成六步；OpenAI 的分析案例则强调发现与核验拆开。本页把两者收成适合计量教师的工作流，并列出常用策略。方法总图见 路线图。

1 总流程

flowchart TB
  src["hansenEM 原文"] --> inv["inventory<br/>定理清单"]
  inv --> l1["L1 教学展开"]
  l1 --> stmt["形式陈述"]
  stmt --> skel["sorry 骨架"]
  skel --> lem["引理 / Mathlib"]
  lem --> fill["填证明"]
  fill --> build["lake build"]
  build --> ax["#print axioms"]
  ax --> cross["对照表回写 inventory"]

原则：一次只钉一条定理（或一条引理链）。整章综述无法验收。

2 步骤 1：原文与 inventory（定理清单）

打开 hansenEM/chapters_eng 对应章，抄下：

• 定理 / 定义 / 假设编号与印刷陈述
• 证明里「于是 / 显然」跳过的步骤
• 用到但未编号的正则条件（独立同分布（i.i.d., independent and identically distributed）、矩、满秩、可测性）

写入本仓库的章清单（路线图建议 inventory/chNN.md，需要时再加）。空单元格表示未做，禁止虚构 Lean 名。lean-hansen-econometrics 把 inventory/chN-inventory.md 当作覆盖率真相源，我们采用同一纪律。

发现印刷陈述过强或有误时，inventory 分三列：字面陈述 / 拟采用的陈述 / 诊断或反例。不要在 L1 里静默改写。

3 步骤 2：L1 必须先于 L3

机器不能替你决定「Hansen 的 \(E(Y\mid X)\) 是条件期望还是线性投影」。先用 Quarto 写人读的展开：对象、维持假设、引理、逐步推导、对照。模板见方法页。

这一步常会改变你对形式化目标的选择。例如第 3 章 Frisch–Waugh–Lovell（FWL）定理：是证投影代数恒等式，还是证「省略变量后系数的数值公式」？两者 Lean 声明不同。

4 步骤 3：陈述工程

把 L1 译成类型签名，比写证明更决定成败。清单：

1. 对象的类型：矩阵 Matrix n k R、随机元 Ω → ℝ、还是已商掉零测集的 L¹？
2. 量词顺序：\(\forall \beta\) 在积分外面还是里面？
3. 几乎处处：等式是 = 还是 =ᵐ[μ]？
4. 全函数化：\((X'X)^{-1}\) 在奇异时：拒绝定义 / 用 nonsingInv / 规定为 0？
5. 假设是否可计算地检查：满秩是 Prop；样本量 \(n\ge k\) 也是。

lean-hansen-econometrics 对有限样本普通最小二乘（OLS, Ordinary Least Squares）给出三种包装：Base（要求可逆）、Star（奇异时走伪逆式引擎）、OrZero（教材对外表面）。渐近证明用 Star，章末可引用陈述用 OrZero。这是陈述工程，不是三种不同的数学真理。

Deng 与 Shum 把对接教材与 Mathlib 的引理叫 bridge（桥接引理）(Deng 和 Shum 2026年)。计量里典型的桥：Hansen 的 \(E(Y\mid X)\) ↔︎ condExp m μ Y（m 为 \(X\) 生成的子 σ-代数）。

5 步骤 4：sorry 骨架

先写：

theorem hansen_fwl ... : ... := by
  sorry

让声明通过精化，再在证明里把 sorry 拆成若干 have + 子目标。Lean 会警告 sorry；#print axioms 出现 sorryAx 即未完成。骨架的价值是：团队可以并行填引理，而不争论定理名叫什么。

不要把含 sorry 的声明对外说成已证明。inventory 应诚实记录剩余缺口。

6 步骤 5：查找，而不是重写分析

填证明前先搜 Mathlib：

• 文档：https://leanprover-community.github.io/mathlib4_docs/
• Loogle：https://loogle.lean-lang.org/（按类型搜索 Mathlib 引理）
• Zulip：https://leanprover.zulipchat.com/（Lean 社区聊天室；学习页强烈建议加入 (Lean prover community 2025年)）
• 编辑器里 #check、按定义跳转、exact? / apply? / rw?（可用性随版本变化）

自己重证塔性质几乎总是错的工作分配。正确工作是：找到 condExp 的引理，再写 10 行包装让它看起来像 Hansen 定理 2.x。

7 常用策略（最小集）

Theorem Proving in Lean 4 的策略章把策略定义为「描述如何构造证明项的命令」(Avigad 等 2025年)。计量入门够用的一组：

策略	课堂对应
intro / rintro	设……；打开 \(\forall\) 与 \(\to\)
apply	用某引理，倒推充分条件
exact	当前目标正好是这项
have / let	中间断言
rw / rewrite	用等式改写
simp	按引理集化简
calc	链式计算，最像 LaTeX 对齐证明
constructor	证合取、结构体
cases / rcases	对存在、析取、结构分情况
refine	先填洞，再逐个打
sorry	占位；必须消灭

calc 值得对教师单独强调：它让 \(A=B=C\) 的板书计算变成可逐步检查的块，是 LaTeX 推导迁移成本最低的策略。

8 步骤 6：构建、公理、回写

本地验收：

lake exe cache get
lake build

对刚完成的定理：

#print axioms my_theorem

把结果写回 inventory：Lean 声明名、文件路径、依赖公理、与印刷陈述的差异。lean-hansen 另有 redundancy / hygiene / faithfulness / proof-quality 四维审阅（冗余、卫生、保真、证明质量）；我们规模较小时，至少做 faithfulness（是否还是那条定理）和 sorry 清零。

CI（Continuous Integration，持续集成）在将来的独立 Lean 仓库里跑同样命令。不要让 Quarto 站点构建去编译 Mathlib。

9 与 Cursor / Agent 的分工

适合自动化的：打开 hansenEM 摘假设、搜 Mathlib 引理名、把 L1 的 calc 链改写成草稿。

必须人审的：形式陈述是否过强、sorry 是否藏在依赖里、对外一句「证明了定理 X.Y」是否越界。

不适合本项目的：上万智能体并发搜证明。路线图已写明。

10 一张工作单（复印用）

对象：Hansen 定理 X.Y（章 NN）
原文路径：hansenEM/chapters_eng/chptNN-....qmd
L1 笔记：
拟 Lean 名：
类型草图：（对象 / 几乎处处 / 可逆性）
Mathlib 入口：
骨架文件：
剩余 sorry：
#print axioms：
与印刷陈述的差异：

下一篇解释这些输出该如何对外讲述，以免「lake build 绿了」被听成「教材整章已证」。

参考文献

Avigad, Jeremy, Leonardo de Moura, Soonho Kong, 和 Sebastian Ullrich. 2025年. Theorem Proving in Lean 4. https://leanprover.github.io/theorem_proving_in_lean4/.

Deng, Shuo, 和 Kenneth Shum. 2026年. From Lecture Notes to Lean: Formalizing a Textbook on Probability Theory. https://arxiv.org/abs/2607.27298.

Lean prover community. 2025年. Learning Lean 4. https://leanprover-community.github.io/learn.html.