守株阁

Lean 4 的 tactic 不是黑盒——每个 tactic 本质上是一段操作证明状态的程序。本篇拆解这套元编程基础设施：Expr 是表达式的内存表示，MVarId 标识待填充的证明目标，MetaM 和 TacticM 是承载副作用的 monad 栈。理解这三层之后，自定义 tactic 就不再是猜测 API 的过程。 Expr：表达式的内部表示 Lean 4 中一切类型、命题、证明项统一表示为 Expr。核心构造子（简化版）： 12345678910111213inductive Expr where | bvar : Nat → Expr -- 局部绑定变量（de Bruijn index） | fvar : FVarId → Expr -- 自由变量 | mvar : MVarId → Expr -- 元变量（待填充的洞） | sort : Level → Expr ...

Mathlib4 提供了一套完整的有限集合与大算子（BigOperators）机制，使得组合数学和初等数论的形式化证明可以在接近数学原文的符号层面进行。Finset 表示有限集合，Fintype 约束类型的有限性，BigOperators 引入求和与连乘的紧凑记号，Nat.Prime 与 Nat.primeFactorsList 覆盖自然数素数理论的基本引理。本篇在此基础上，进一步介绍 decide tactic 在有限域穷举中的作用，以及 Decidable 类型类的内部逻辑。 前置阅读：02 Term-mode 与 Tactic-mode 切换心法（tactic 基础）；04 核心 tactic 精讲（rfl、ring、omega 等基础 tactic）；05 simp 与 norm_num（自动化 tactic）。 Finset 与 Fintype Finset 的数据表示 Finset α 是 Mathlib4 中对有限集合的主要表示，定义于 Mathlib.Data.Finset.Basic： 123structure Finset (α : Type*) where...

Mathlib 的分析库以 Filter 为核心抽象，在此之上叠加拓扑、度量和赋范结构，统一表达极限、连续、收敛等概念。理解这套分层设计，是读懂 Mathlib 分析证明的前提。本篇梳理 Filter、TopologicalSpace、MetricSpace 和 NormedSpace 四层结构的定义方式和证明惯用法，并通过具体可运行代码展示各层之间的关联。 前置阅读：本系列 09 Mathlib 搜索技巧、10 类型类层次、11 在 Mathlib 上证一个小定理。 Filter：分析库的基础抽象 为什么不直接用 ε-δ 经典分析教材用 ε-δ 定义极限：对每个 ε > 0，存在 δ > 0，使得……这个定义能精确刻画单个极限，但在证明库里它有两个缺陷。第一，同一个"极限"概念在不同情形（趋向实数点、趋向无穷、序列极限、网极限）下需要写出形状不同的 ε-δ 公式，导致同一条定理（如极限的线性性）在每种情形下各需一个版本。第二，组合两个极限结论时，条件匹配需要手动传递 ε/2 技巧，证明文本冗长。 Mathlib 选择用 Filter 把&quo...

向 Mathlib 贡献一条引理，从选题到合并大约需要经历六个阶段：确认缺口、搜索已有引理、写证明、通过本地 lint、跑通 CI、完成 PR 审核。本文以一个具体的 List 辅助引理为例，完整走一遍这条路径。 选题：找一个真实的缺口 Mathlib 的条目超过十五万条，盲目选题很容易踩在别人已经证过的结论上。有效的选题通常来自两个方向：一是在自己的项目里遇到 exact? 无法命中的目标；二是在 Zulip 的 #mathlib4 频道里找标了 easy 标签的 issue。 本文选用的定理是 List.length_zipWith，即： 12∀ (f : α → β → γ) (l₁ : List α) (l₂ : List β), (List.zipWith f l₁ l₂).length = min l₁.length l₂.length 在实际的 Mathlib 里，这条结论已经存在（List.length_zipWith），但选它作例子的原因是它足够小、结构清晰，可以完整演示所有步骤，而不会把证明本身的复杂度淹没流程细节。实际投稿时，需要找 Mathlib 确实...

Lean 4 的类型类机制是整个 Mathlib 代数层次的基础设施。从 Monoid 到 Field 的继承链、instance 搜索的 backtracking 算法、以及钻石问题的处理方式，这些设计决策共同决定了 Mathlib 4 能否在百万行规模下保持一致性。本篇专注于类型类层次本身：class/instance/extends 三个关键字的语义、Mathlib 代数 hierarchy 的组织方式、instance 搜索的调试手段，以及如何编写自定义类型类并纳入现有层次。 class 与 instance：基础机制 Lean 4 的类型类是一种特殊的 structure，由 class 关键字声明。编译器对它的处理与普通 structure 的差异在于：class 的实例由 instance 合成器（synthesis engine）自动查找，而不需要显式传入。 12345678910-- 声明一个类型类：具有幺元class HasOne (α : Type*) where one : α-- 为 Nat 注册实例instance : HasOne Nat whe...

Mathlib4 截至 2024 年末已收录超过 16 万条定理、引理和定义。面对这个规模，手工翻阅文档或凭经验猜名字的效率极低。Lean 4 工具链和 Mathlib 生态提供了一套完整的搜索机制：从编辑器内的 exact?、apply?、rw?、simp?，到浏览器端的 Loogle 和 Moogle——每种工具针对不同的查询意图。掌握这套机制是高效使用 Mathlib 的基本工作方式。 本篇是"深入 Lean"系列第 09 篇。前置阅读：04 核心 tactic 精讲（exact/apply/rw 的语义）、05 simp 与 norm_num（simp 引擎工作原理）、02 Term-mode 与 Tactic-mode 切换心法（两种证明模式的区别）。 问题规模 Mathlib4 的 GitHub 仓库目前约有 70 万行 Lean 代码，模块数量接近 4000。定理覆盖了代数、数论、分析、拓扑、组合、范畴论等数十个领域。一条具体的引理，如 List.length_append 或 Nat.add_comm，隐藏在数百个文件中的某一处。 这个规模带...

Lean 4 的 tactic 框架不是封闭的黑盒——整个 tactic 集合本身就是用 Lean 4 写成的，对用户完全开放扩展。syntax、macro、elab 三个关键字构成了这套元编程机制的核心，分别对应语法解析层、宏展开层、精化（elaboration）层。理解这三层的职责边界，就能在合适的抽象层次上定义自己的 tactic，而不是绕道求助 sorry 或重复编写机械的组合步骤。 本篇是"深入 Lean"系列第 08 篇。前置阅读：02 Term-mode 与 Tactic-mode 切换心法（tactic 基本操作），03 Universe 与类型层级实战（Sort/Type/Prop 区分）。 三层架构 Lean 4 的元编程体系在编译管线里分三层处理用户写下的语法片段： 1234567用户源码 ↓ 解析（parser）语法树（Syntax） ↓ 宏展开（macro expansion）展开后的语法树（Syntax） ↓ 精化（elaboration）核心项（Expr） 解析层由 syntax 关键字负责，扩充 Lean 的文法，告诉解...

rw 按从左到右的顺序匹配第一个符合的子项并替换，simp 则对所有可匹配位置做化简。两者在精度上处于两个极端：一个只打第一枪，一个全部扫射。实际证明中经常需要介于两者之间的操作——精确指定重写位置。Lean 4 提供了 conv 和 calc 两套工具：conv 在目标的语法树上导航到具体子表达式再执行重写，calc 把一串等式或不等式推导组织成可读的链式结构。 本篇的前置知识是 rw、simp 的基本用法（见第 04 篇：核心 tactic 精讲和第 05 篇：simp 与 norm_num）。所有代码在 Lean 4 v4.12.0 + Mathlib4 下通过 lake build 验证。 conv 的基本结构 conv 开启一个子目标编辑会话。在这个会话内，当前目标被视为一棵语法树，通过导航组合子定位到具体子表达式后再执行操作。 最简单的例子：目标是 ⊢ 0 + n = n，想用 Nat.zero_add 重写左侧。在更复杂的情况下等号两侧可能都包含相同的子项，此时需要限定重写范围。 12example (n : ℕ) : 0 + n = n := by conv_l...

在形式化方法系列的前几篇中，从类型论基础（01）、目标窗口与 tactic 交互模型（02）到 Gallina 核心语法（03）、基础 tactic 全景（04）以及搜索与自动化（05），关注点始终落在"如何与 Lean 的类型检查器对话"。本篇收窄焦点：当证明目标是算术命题时，四个专用 tactic 各自覆盖哪个数学域，各自在哪里失效。 这不是一个"哪个 tactic 更强"的比较，而是四个具有严格数学边界的决策过程的并排描述。选错工具只会让证明永远挂起或留下 sorry，而不会神奇地奏效。 omega：Presburger 算术的完备决策器 覆盖范围 omega 实现了 Presburger 算术（Presburger arithmetic）的完备决策过程。Presburger 算术是一阶逻辑中关于自然数和整数的理论，限定以下运算： 加减法（+、-） 整数常量乘法（n * x 其中 n 是字面整数） 整除与取模（%、/） 比较运算（<、≤、=、≠） 对 Nat 和 Int 类型的线性整数命题，omega 要么给出证明，要么报告...

simp 和 norm_num 是 Lean 4 / Mathlib4 中使用频率最高的两个自动化 tactic。simp 是一个基于重写规则集合的项化简引擎，norm_num 是一个针对数值表达式的可判定算术归一化器。理解这两个 tactic 的工作原理，对于写出既正确又可维护的 Mathlib 风格证明至关重要。 前置阅读：本系列 02 Term-mode 与 Tactic-mode 切换心法 讲解了 tactic 块的基本结构；03 Universe 与类型层级实战 阐述了 Prop 与 Type 的区别——这些背景在理解 simp 的化简对象范围时用得上。 simp 的重写引擎 合流重写系统 simp 的核心是一个合流项重写（confluent term rewriting）系统。给定一组重写规则，系统对当前目标反复应用规则，直到没有规则可再适用为止。"合流"意味着：无论规则的应用顺序如何，最终结果（正规形式，normal form）是唯一的。 Lean 4 中，每条重写规则形如： 1lhs = rhs simp 将目标中所有能匹配 lhs 的子项替...