writing-lean-proofs

编写 Lean 证明

目录

• 何时使用
• 何时不使用
• 工作流
• 提取阶梯
• 快速参考
• 应拒绝的托辞
• 参考资料

对 Lean 4 证明编写和库设计进行结构化梳理，内容提炼自 Mathlib 的风格和评审惯例，以及大型形式化项目（Liquid Tensor Experiment、PFR、费马大定理）的方法论。

核心原则：自顶向下设计，自底向上证明。 Lean 命题具有证明无关性——只有定理的陈述会影响后续声明。陈述是稳定的接口；证明则可以舍弃并自由替换。应将设计精力投入定义和陈述，然后针对已经可以编译的框架（允许使用 sorry）补全证明。

何时使用

• 在 Lean 4 中证明定理，从单个引理到多文件开发
• 在 Lean 中形式化数学、协议或软件规范
• 在 Lean 库中定义新类型、结构或函数
• 评审 Lean 代码的可读性、可维护性或是否符合 Mathlib 规范
• 将冗长或脆弱的策略证明重构为引理
• 为多个成员或 Agent 将并行参与的形式化项目搭建框架
• 为 Lean 项目设置 CI、代码检查工具或验证关卡——应在项目启动时完成，以免不良模式扩散
• 诊断缓慢的证明、maxHeartbeats 超时或开销高昂的归约
• 编写自定义策略、宏或项目专用代码检查工具

何时不使用

• 将 Lean 4 用作通用编程语言（不涉及证明）——本技能的大部分内容都针对证明和 API 结构
• Coq、Isabelle、Agda 或 Lean 3——惯例和策略名称各不相同；Lean 3 的惯用模式（ge_or_gt 代码检查、discrete_field）已过时
• 有自身风格规范的 Lean 验证软件项目（例如优先追踪规范的代码库）：Mathlib 惯例是社区默认标准，但请先查阅项目的 CONTRIBUTING，并以项目规范为准

工作流

1. 先设计定义及其 API

定义承载着主要设计工作。在证明新概念的任何性质之前：

• 优先使用带有无用值的全函数，而不是在签名中使用子类型或 Option（Mathlib：(0 : ℝ)⁻¹ = 0）。这样，侧条件只会出现在需要它们的引理中，而不必在每个使用位置都出现。
• 使用结构体封装：新类型的态射应为带有 FunLike 实例的结构体；新类型的子对象应使用 SetLike；将性质证明作为结构体字段携带，而不是定义单独的 IsHom 风格谓词。
• 为每个有多种等价形式的概念选定规范写法（simp 标准形式），并且只针对这种形式陈述所有 API 引理。
• 立即在同一文件中编写 API：在定义于任何地方使用之前，先编写 ext、@[simp]、强制转换和单射引理。下游证明应使用 API，绝不使用 unfold / show ... from rfl。

完整的设计规则及其理由，请参阅 library-design.md。

2. 构建 sorry 框架

先陈述所有内容，再证明任何内容，并且在每个层面都如此：

• 项目层面：陈述目标定理及其所需引理，全部使用 := sorry，并确保文件可以编译。此时每个 sorry 都是一个独立的工作单元——贡献者（人类或大模型）无需理解其余部分，就能补全其中一个。这正是 LTE、PFR 和 FLT 能够扩展到数十名并行贡献者的方式。
• 证明层面：在证明内部，用 sorry 作为依据，搭建 have / suffices / calc 框架，让 Lean 接受其结构，然后逐步补全。保持结构不变，才能在编写过程中获得有用的错误消息。

example (a b c d : ℝ) (h : c = d * a + b) (h' : b = a * d) : c = 2 * a * d := by
  calc
    c = d * a + b     := sorry
    _ = d * a + a * d := sorry
    _ = 2 * a * d     := sorry

3. 填写目标，一次专注于一个目标

• 每个新子目标都要用聚焦点 · 和缩进代码块来处理——绝不要让多个目标连续处于未聚焦状态（Mathlib 的 multiGoal 检查器会强制执行这一点）。这正是消除脆弱的目标顺序依赖的方法。
• 每个代码块开头都要用冗余的 show 声明目标。证明本身不需要它，但审阅者和未来的编辑者需要。如果 show 会改变目标，则改用 change——确保声明的目标准确无误。
• 等式或不等式的连续改写应写成 calc 代码块，并将关系符纵向对齐。
• 用 have 表示向前推进的中间步骤（“我们先证明 X”）；用 suffices 表示向后化简（“只需证明 X”）。
• 起草时，在不明显的策略之前用注释标注目标状态——内容必须由 Lean 输出，不能凭空想象。在无头工作流中，在关注的位置插入 trace_state，或在目标本应关闭的位置有意插入 done，然后运行 lake env lean Path/To/File.lean；复制报告中的假设、分支名称和目标。证明成功后，删除常规探测代码。这是编写 Lean 证明的 LLM 最有效的技巧（参见 llm-techniques.md）。

完整的策略风格规则见 proof-style.md；关于如何命名引理，使其名称能从陈述中推测出来，见 naming-conventions.md。

4. 机械验证

不要凭肉眼检查风格——运行检查器。lake build 是最低要求，而且仅仅是最低要求：sorry 只是警告，因此即使仍有 sorry，绿色构建也会以状态码 0 退出。

• 通过询问内核来检查未证明的义务，绝不要靠 grep。 可用 #print axioms myTheorem 抽查；对于 CI，使用 Lean.collectAxioms 收集每个声明的公理，并断言完整的预期范围（除非有意扩大，否则为 [propext, Classical.choice, Quot.sound]），这样意外的 sorry 或 native_decide 之类新增的信任假设都会明确报错。Grep 在两个方向上都不可靠：它会匹配注释中的单词，也会漏掉自身文本干净、但使用了未证明辅助引理的定理。可用脚本见 linting.md。
• 根据项目角色选择检查项，并在项目启动时将它们加入 CI。 下游项目不要整体启用 linter.mathlibStandardSet：它混合了证明维护检查、公共 API 检查、内部风格和 Mathlib 特定的仓库政策。对于独立证明，可从 linter.auxLemma、linter.style.maxHeartbeats、 linter.style.multiGoal、linter.style.setOption 和 linter.style.show 开始。可复用库还应启用 linter.flexible、 linter.style.missingEnd、linter.style.openClassical 和两个 unused*InType 检查。将 nativeDecide 视为信任政策选项，将格式或已弃用语法检查视为项目风格。除非警告会导致构建失败，否则没有警告能阻止任何操作。另行运行 Batteries 的声明级 #lint 检查，包括 simpNF。根据固定版本的 Mathlib 源码验证每个选项，并用已知触发示例进行验证：拼写错误的 weak. 选项会被有意忽略。完整的 26 项审计和 lakefile 配置见 linting.md。
• 为每项项目特定约定编写自定义检查器（simp 集合规范、摘要引理覆盖率、必需属性）——声明级 @[env_linter] 是一种结构，也是唯一能可靠捕获“30 个声明中有 29 个缺少该属性”的方式。编写方法和工程规则（空洞锚点、证明检查器确实能失败、允许列表）见 linting.md。

抽取阶梯

证明结构何时应拆分为独立引理？

0. 抽取之前，先说明片段的类型，并按形状搜索。 将拟定的陈述放入临时 example，在裸目标上运行 exact? 和 apply?，然后尝试类型模式搜索和源码搜索。如果有现成定理适用，就使用它。若未记录失败的搜索，不要声称 API 存在缺口。

1. 某个子论证在同一个证明中重复出现 → 将其命名为局部 have。

   theorem min_comm (a b : ℝ) : min a b = min b a := by
     have h : ∀ x y : ℝ, min x y ≤ min y x := by
       intro x y
       apply le_min
       · show min x y ≤ y
         exact min_le_right x y
       · show min x y ≤ x
         exact min_le_left x y
     apply le_antisymm
     · show min a b ≤ min b a
       exact h a b
     · show min b a ≤ min a b
       exact h b a
   

2. 该陈述本身具有独立意义，或者抽取后能去掉子论证不需要的假设 → 独立引理。去掉不需要的假设是更有力的触发条件：抽取出的引理会比其来源证明更通用。

3. 证明读起来「冗长繁琐」 → 拆分它。这是 Mathlib 的评审标准，而且有意保持定性——没有行数门槛。有疑虑时就尝试抽取：如果某个片段能清楚地表述出来，那它就适合成为引理。

快速参考

规则	原因	执行方式
下游代码中绝不展开定义；erw 或末尾的 rfl = 缺少 API	API 引理是抽象边界	评审（「缺少 API」异味）
终结位置的 simp 不要收缩；非终结位置的 simp 改为 simp only [...]	收缩后的终结调用会掩盖关键引理，并在重命名时失效	风格指南
一次只处理一个聚焦目标（· 块）	消除目标顺序导致的不稳定性	linter.style.multiGoal
show 不得改变目标（使用 change）	明确写出的目标必须忠实	linter.style.show
最终代码中不得包含调试/跟踪/分析器用的 set_option，也不得包含无作用域限定的 maxHeartbeats	调试脚手架	linter.style.setOption
以 simp 规范形式陈述引理，使用 < 而非 >	simp 按语法形式匹配	simpNF linter
仅当结果至少同样易读时才缩短；平凡结果除外	短不等于更好	评审
Fact 实例必须是局部的，绝不能是全局的	全局实例会降低所有类型类搜索的效果	评审
根据陈述为引理命名（参见命名参考）	让人无需搜索也能猜出名称	linter.style.nameCheck 只检查 __；#lint defsWithUnderscore 和评审会覆盖更多情况
编写辅助引理或声称 API 存在缺口之前，先按形状搜索裸目标	目标不一定能让人猜出名称	exact?、apply?、类型/源码搜索
通常每行只调用一个 tactic；单行结束证明是例外	保持证明结构易读，同时不臆造绝对规则	风格指南
用 collectAxioms/#print axioms 检查 sorry，绝不使用 grep	grep 会匹配注释，却会漏掉未证明的辅助项	CI 中的公理审计
优先使用以结构而非数字为键的 simp 引理左侧；每个常量只采用一种写法	2 ^ 32 永远无法匹配规范化为 4294967296 的目标	simpNF、评审
在每个 simp only 列表所在的位置，都用 simp? 重新推导	相似目标之间无法直接复用列表	linter.flexible
每个 maxHeartbeats 覆盖值都是尚未证实的断言——先测量，再相信	复制粘贴的预算毫无信息	#count_heartbeats、二分查找
条件 simp 引理浅层能触发、深层却不能触发 → 提高 maxDischargeDepth（默认值为 2）	链式前提条件会悄然截断，且没有诊断信息	诊断（证明风格、simp 纪律）
每项项目专属约定都要配备自定义 linter，并从第一天起纳入 CI	评审无法发现 30 次中失败 29 次的情况	@[env_linter] + #lint

每一行的完整理由，以及库级反模式，见 anti-patterns.md。

应当驳斥的借口

借口	事实
“证明能编译，提交吧”	能编译只是最低要求。只有 Lean 才能读懂的单体 tactic 代码块，会在下一次 Mathlib 更新时悄无声息地失效，而且没人能修复它。
“展开定义比写 API 引理简单”	每个下游的 unfold 都会让证明与实现耦合。第一次重构就会让它们全部同时失效。把缺少的引理写出来。
“把每个 simp 都压缩起来，证明会更快、更稳健”	对终结性 simp 调用来说，恰恰相反：压缩后的列表会在每次重命名时失效，还会淹没关键信息。只压缩非终结性调用。
“越短越好”	Mathlib 的审查政策是：只有在不牺牲可读性的前提下，精简代码才可以。目标不是长度，而是清晰易读。
“等它能用了，我再把它重构成引理”	等它能用时，结构就已经成了不可或缺、错综复杂的一部分。先写出骨架；引理自然就会浮现。
“添加 show 行是多余的噪声”	对内核来说它们是多余的，对接下来阅读证明的每个人或模型来说却不可或缺。
“这个辅助定理太具体，不适合作为引理”	只要它有清晰的陈述，就把它提取出来——去掉它不需要的假设，通常就会发现它原本一直都足够通用。
“等库稳定后再添加 linter”	恰恰相反：模式会通过复制粘贴传播，因此延后的 linter 面对的将是 400 条警告，而不是一行错误代码。现在就启用已有的干净规则并设置门禁。
“检查通过了，所以代码没问题”	无法失败的检查毫无证明力——扫描可能因文件数归零而通过，拼错的 weak. 选项可能被忽略，管道可能吞掉退出码。在相信检查通过之前，先证明每个门禁都能失败。
“证明太慢了，调高 maxHeartbeats”	未测量的预算只是主张，不是修复——而且它会掩盖下一位读者需要看到的性能退化。使用 #count_heartbeats 进行测量；重构定义或分解目标。

参考资料

• library-design.md — 定义、API、 打包、抽象边界、由规格驱动的项目分解
• proof-style.md — tactic 证明结构： calc、have/suffices、聚焦，以及 simp 规范，包括“为什么这个引理没有触发”的 诊断（消解深度、遍历顺序、数字字面形式）
• naming-conventions.md — Mathlib 命名 规范，使引理名称可以根据陈述推导出来
• anti-patterns.md — 已知反模式、 各自有害的原因，以及能捕获它们的 linter
• llm-techniques.md — 针对大模型编写证明的、 基于证据的技巧
• linting.md — 基于公理的 sorry 门禁、尽早在 CI 中启用 项目专用的 linter 配置文件、完整的 Mathlib 标准规则集 审计、在存在积压时引入 linters、为 项目专用结构编写自定义 linters，以及证明每个门禁都能失败
• performance.md — 衡量每个声明的 开销、归约开销的来源，以及在不丢失语义的前提下优化定义
• tactics.md — 元编程规范： 扩展点选择、元变量与恢复保护、有界 搜索、可操作的错误、结构化跟踪、生成的声明， 以及失败场景测试