深入 Lean 18：Lean 4 证明工程总结与路线图

本篇回顾系列的整体脉络，指出从当前知识基线出发的进阶路线，并以一个综合验证项目作为收束。

系列脉络回顾

第 01-03 篇建立工具链基础：Lake 项目结构与依赖管理（01）、term-mode 与 tactic-mode 的切换心法（02）、universe 与类型层级（03）。核心技能在这一阶段成型——配置 lakefile、读懂 InfoView 目标状态、在 term-mode 和 tactic-mode 之间做有意识的选择。

第 04-08 篇深潜 tactic 系统：核心 tactic 精讲（04）、simp 与 norm_num 重写引擎（05）、算术自动化族（06）、conv 与 calc 精确重写（07）、自定义 tactic 与宏（08）。这些工具覆盖了日常证明的绝大部分需求。

第 09-13 篇连接 Mathlib 生态：搜索技巧（09）、类型类层次（10）、端到端贡献流程（11）、拓扑与分析结构导览（12）、有限组合与数论（13）。读者到这一阶段能在 Mathlib4 上独立工作。

第 14-17 篇进入元编程领域：Expr/MVarId/MetaM 模型（14）、elaborator 与 command 编写（15）、Aesop 声明式自动化（16）、可执行代码与 FFI（17）。自定义语法和自动化策略的能力在这里建立。

进阶方向

LeanSAT：SAT/SMT 集成

LeanSAT 把 SAT 求解器（如 CaDiCaL）集成到 Lean 4 的证明系统中。对于有限命题或位向量相关的目标，LeanSAT 能自动决策：

import LeanSAT

example (a b c : Bool) : (a || b) && (!a || c) → (b || c) := by
  decide  -- 对小规模 Bool 命题直接穷举

LeanSAT 的核心价值在于处理 decide 无法承受的规模——通过调用外部 SAT solver 获取反例或 UNSAT 证书，再在 Lean 内部验证该证书。这种"计算外部化、验证内部化"的架构保证了可信度。

入口建议：LeanSAT 仓库的 README 和 examples 目录。

ProofWidgets4：交互式可视化

ProofWidgets4 把 React 组件嵌入 Lean 4 的 InfoView，让证明状态的展示不限于纯文本。典型应用：

几何证明中显示图形
组合证明中显示图的邻接结构
展示 tactic 搜索树的可视化

import ProofWidgets

-- 在 InfoView 中渲染自定义 HTML
#html <div style="color: blue">Hello from ProofWidgets</div>

ProofWidgets4 的底层通过 Lean 4 的 widget 框架工作——@[widget_module] 注册一个 JavaScript 模块，InfoView 的 VS Code 扩展负责渲染。

入口建议：ProofWidgets4 文档。

SciLean：科学计算的形式化

SciLean 在 Lean 4 上构建可微编程和科学计算的形式化框架。核心特性：

自动微分（AD）的形式化：前向模式和反向模式 AD 的正确性证明
函数空间上的运算：梯度、散度、旋度的符号计算
与数值计算的桥接：经过验证的数值方法可以提取为可执行代码

SciLean 展示了 Lean 4 "程序即证明"统一性的极限应用——同一套代码既是数学定义，又是可执行的数值算法，同时附带正确性证明。

入口建议：SciLean 仓库和附带的 tutorial notebook。

Lean 4 与 AI 集成

LeanDojo 和 ReProver 把大语言模型接入 Lean 4 的证明搜索循环：

LeanDojo 提供 Lean 4 环境的 Python 接口，允许 LLM 观察目标状态并生成 tactic
ReProver 在 LeanDojo 基础上训练了 retrieval-augmented 的证明生成模型
COPRA 使用 GPT-4 作为 tactic 建议器，配合 Lean 4 的类型检查做 verify-and-retry 循环

这些工具目前处于研究阶段，尚未达到生产可靠性。但方向清晰：LLM 负责"猜"tactic，Lean 内核负责"判"对错，两者互补。

入口建议：LeanDojo 论文与代码。

工具链资源

资源	用途
Lean 4 Zulip	社区问答，核心开发者活跃
Mathlib4 文档	16 万+ 定理的 API 文档
Loogle	按类型签名搜索 Mathlib 引理
Lean 4 Web	浏览器内 Lean 4 环境
Mathematics in Lean	系统教程，覆盖数学各分支
Metaprogramming in Lean 4	元编程专题

综合验证项目

作为系列收束，下面是一个覆盖多篇主题的综合项目。

实现并验证一个简单的表达式编译器。定义 AST 和语义：

inductive Expr where
  | const : Nat → Expr
  | plus  : Expr → Expr → Expr
  | times : Expr → Expr → Expr

def Expr.eval : Expr → Nat
  | .const n     => n
  | .plus e1 e2  => e1.eval + e2.eval
  | .times e1 e2 => e1.eval * e2.eval

定义栈机和编译器：

inductive Instr where
  | push : Nat → Instr
  | add  : Instr
  | mul  : Instr

abbrev Prog := List Instr
abbrev Stack := List Nat

def run : Prog → Stack → Option Stack
  | [],            s          => some s
  | .push n :: p,  s          => run p (n :: s)
  | .add :: p,     b :: a :: s => run p ((a + b) :: s)
  | .mul :: p,     b :: a :: s => run p ((a * b) :: s)
  | _ :: _,        _          => none

def compile : Expr → Prog
  | .const n     => [.push n]
  | .plus e1 e2  => compile e1 ++ compile e2 ++ [.add]
  | .times e1 e2 => compile e1 ++ compile e2 ++ [.mul]

目标定理：

theorem compile_correct (e : Expr) :
    run (compile e) [] = some [e.eval] := by
  have h := compile_correct_gen e [] []
  simp [List.append_nil] at h
  exact h

直接对 e 归纳会在 plus 情况卡住——归纳假设只谈空栈。泛化辅助引理：

theorem compile_correct_gen (e : Expr) (p : Prog) (s : Stack) :
    run (compile e ++ p) s = run p (e.eval :: s) := by
  induction e generalizing p s with
  | const n => simp [compile, Expr.eval, run]
  | plus e1 e2 ih1 ih2 =>
    simp only [compile, Expr.eval, List.append_assoc]
    rw [ih1]
    rw [ih2]
    simp [run]
  | times e1 e2 ih1 ih2 =>
    simp only [compile, Expr.eval, List.append_assoc]
    rw [ih1]
    rw [ih2]
    simp [run]

验证无公理依赖：

1
2
3

#print axioms compile_correct
-- 'compile_correct' depends on axioms: [propext, Eq.mpr, ...]
-- propext 和 Eq 相关公理是 Lean 4 核心的一部分，可接受

扩展方向：添加变量绑定（let x := e1 in e2）。这需要引入环境（List Nat，按 de Bruijn index 访问）和一条 store 指令。重新证明编译正确性时，泛化引理需要同时携带环境参数。添加条件分支（ifZero e1 then e2 else e3）则需要在栈机中增加跳转指令，证明难度进一步上升。

这个项目综合运用了归纳法（第 04 篇）、simp 引擎（第 05 篇）、列表相关引理搜索（第 09 篇）、generalizing 关键字（第 04 篇的归纳法加强形式）。