如何解读形式化结果

内核通过、sorry、公理与陈述保真

形式化最容易被误读的一点：绿色的构建日志看起来像「数学被解决了」。内核只回答一个窄问题——这个声明的类型是否由这些公理推出。它不回答「声明是不是教材原句」，也不回答「假设在数据里是否成立」。本页给教师一套对外解释的词汇。OpenAI Navier–Stokes（NS，纳维–斯托克斯）案例与 lean-hansen-econometrics 的资格说明，是两份现成教材。

1 内核实际担保什么

当 lake build 成功且目标定理的证明项不含 sorry 时，可以诚实说：

在 Lean 4 某版本、Mathlib（Lean 的数学库）某修订、以及 #print axioms 列出的公理下，声明 Foo.bar 被内核接受。

这句话已经很长，却仍然比「我们形式化了第 4 章」短而精确。拆开看：

  • 版本：换工具链后需要再构建。证书绑的是锁文件，不是「Lean」这个专名。
  • 声明名：人读定理是 Hansen 4.3；机器读的是某个 theorem。两者靠对照表连接。
  • 公理表：经典分析几乎总会出现 Classical.choice 等，见 类型论与内核。

不能自动推出的：

  • 印刷教材的同一句话为真（可能译错、加强、或改了量词）。
  • 经验模型正确（独立同分布（i.i.d., independent and identically distributed）在样本里成立）。
  • 数值复现（那是实证轨 / L2）。
  • 证明「漂亮」或「与课堂讲法相同」。

2 sorry 与 sorryAx

sorry 用公理 sorryAx 关闭目标。语法上文件可以编译，逻辑上该洞是承认未证。依赖一座含 sorry 的引理，洞会传染。Mathlib 提供 #print sorries 一类命令，用于找「为什么这个声明其实不干净」。

对外沟通：

状态 可说 不可说
仅有 inventory（定理清单） 我们登记了定理 X.Y 已形式化
有 sorry 骨架 声明已写、证明未完成 已验证
sorry 清零、lake build 过 该形式陈述已检查 教材原句已检查（除非对照表论证同义）
公理含 sorryAx 仍未完成 「只差一点点」而不列洞

3 三条标准公理不是丑闻

计量几乎全是经典概率。看到

#print axioms ols_unbiased
-- propext, Classical.choice, Quot.sound

应解释为：证明使用了与日常分析相同的经典逻辑（选择公理、命题外延 propext、商类型 Quot.sound）。这与「用了排中律」同类，不是偷偷引入了新的计量假设。

需要单独披露的：

  • sorryAx
  • native_decide / 编译器求值类公理（信任根扩到运行时）
  • 项目自定义 axiom（等于另开理论）

Navier–Stokes 公开仓库把 propext、Classical.choice、Quot.sound 写进 formalization.yaml，是好习惯：证书与公理表一起发布。

4 陈述缺口：真正的第一风险

形式化失败很少是「内核算错」，更多是「证了另一条定理」。

案例 A：Clay 数学研究所千禧年问题的编号。
OpenAI 2026 年 9 月公布的 Navier–Stokes 结果，按官方说明对应千禧年问题表述中带光滑外力的 C/D，不是无外力的 A/B。内核无法知道 Clay 网页上的「原问题」是哪一款；Comparator（对照检查器）把 Lean 声明接到独立参考陈述，才是针对保真的检查。迁移到计量：对照物是 hansenEM/chapters_eng，不是模型的记忆，也不是中文转述。

案例 B：Hansen 印刷定理过强。
lean-hansen-econometrics 在第 11–13 章公开记录：例如印刷的 Theorem 11.6 目标一般不真，仓库改为可行似不相关回归（SUR, Seemingly Unrelated Regression）协方差的正确对象，并形式化「若坚持印刷目标会推出不合法的普通最小二乘（OLS）/ SUR 等式」；Theorem 12.7 按印刷为假，inventory 区分字面 / 修正 / 诊断端点。这是形式化的科研产出：把教材里的裂缝变成可检查的反例或修正陈述。

因此，任何对外句子都要带一个从句：

我们证明的是 inventory 中「采用的陈述」，它与 Hansen 定理 X.Y 的差异见对照表第 N 行。

没有对照表，就没有「形式化了 Hansen」。

5 de Bruijn 因子与「写了多久」

形式化行数除以人写数学行数，常称为 de Bruijn 因子。液态张量实验（LTE, Liquid Tensor Experiment）中，数页证明可对应数万行 Lean，很大一部分是当时库里没有的范畴论基础设施。因子高，不自动等于定理更深；因子低，也不自动等于更可信。

对计量教师更有用的预算：

  • 代数恒等式（投影幂等、Frisch–Waugh–Lovell（FWL）定理）：库支持好，因子较低，适合当第一条 L3。
  • 条件期望：库有 condExp，但教材记号与几乎处处会拉长桥接。
  • 渐近：需要随机元数组、依测度收敛、Slutsky；声明的假设清单往往长过教材一节。

进度应用「sorry 清零的定理条数 + 对照表覆盖」衡量，不用「仓库行数」或「智能体数量」。

6 如何读别人的 Lean 仓库

打开一个声称形式化某教材 / 论文的仓库时，按这次序读：

  1. README 的资格说明（完成了哪一章？partial 还是 complete？）
  2. lean-toolchain 与 Mathlib 修订
  3. inventory 或 formalization.yaml：印刷编号 ↔︎ 声明
  4. lake build 是否在干净环境下可复现
  5. #print axioms 抽样；搜 sorry
  6. 一两处「修正陈述」是否写明

若 README 没有资格说明，把完成度视为未知。lean-hansen 明确写：第 2–13 章为 partial，第 1、14–29 章仅 inventory，没有任何一章被标成覆盖所有小节、推导、例子与习题。这是可引用的表述。

7 课堂上可以怎么讲

可以用三句话结束一次「什么是形式化」的 15 分钟插播：

  1. LaTeX 证明说服人；Lean 证明说服一台小内核。
  2. 内核通过只说明「这个句子」；句子是否等于黑板上的定理，要靠对照表。
  3. 因此我们继续写 L1，并且在将来只挑少量定理做 L3——不是因为 Lean 不重要，而是因为保真比堆砌 .lean 文件更稀缺。

下一篇把上述标准接到 Hansen 的具体数学对象：条件期望、普通最小二乘（OLS）与渐近。