守株阁

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 的子项替...

Lean 4 的 tactic mode 把证明分解成一系列目标变换步骤。每条 tactic 接收当前的目标状态（一组待证的 ⊢ 句），修改它，产生零个或多个新目标。当所有目标消除完毕，证明关闭。七条核心 tactic——intro、apply、exact、constructor、cases、induction、simp——覆盖了命题逻辑和结构归纳证明的绝大部分场景，各自有精确的语义模型和目标变换规则。 前置阅读：本系列 01 Lake 项目结构与依赖管理、02 Term-mode 与 Tactic-mode 切换心法、03 Universe 与类型层级实战；形式化方法系列 在 Lean 4 中证明经典命题。 intro 语义模型 intro h 处理目标形如 ⊢ A → B 或 ⊢ ∀ x, P x 的情形。它把 goal 的前件或全称绑定变量从目标中移走，引入上下文成为假设，同时把目标替换为后件或实例化的命题。 123456引入前：⊢ A → B执行 intro h 后：h : A⊢ B ∀ 的情形： 123456引入前：⊢ ∀ (n : Nat), n + 0 = n执行...

Lean 4 的类型系统里有一个经常被初学者忽视的维度：每个类型本身也有类型，类型的类型称为 universe（宇宙）。忽视这一维度，往往导致一类难以直觉理解的报错——类型不匹配、universe 不一致、无法做大消除。本篇聚焦 universe 层级的实际操作，包括 Prop 与 Type u 的区别、universe 多态定义、以及常见 universe 错误的诊断方法。 前置阅读：本系列 01 Lake 项目结构与依赖管理 和 02 Term-mode 与 Tactic-mode 的切换心法；形式化方法系列 准备 Lean 4 实验环境。 Universe 层级 Lean 4 的类型层级是一个无穷塔（infinite tower），用 Sort 统一表示： 1Sort 0 : Sort 1 : Sort 2 : Sort 3 : ... Prop 是 Sort 0 的别名，Type 是 Type 0 = Sort 1 的别名，Type 1 是 Sort 2，以此类推。 12345#check Prop -- Prop : Type#check Type ...

Lean 4 提供两种写证明的语法面：term mode 直接给出构造该类型的项；tactic mode 通过一系列指令逐步缩减未完成的目标。两者在语义上等价——任何 tactic 证明最终都被 elaboration 翻译成一个 term，类型检查器只检查 term 层。选择哪种写法是风格决策，但这个决策在实践中有明确的倾向规则。 本篇是"深入 Lean"系列第 02 篇。系列前置知识见《在 Lean 4 中证明经典命题》，该篇已展示了两种模式的基本对照；本篇专注于切换判断本身：什么情况下 term mode 更短、更清晰，什么情况下 tactic mode 更易读、更可维护，以及两种模式如何在同一个证明里混合使用。 Term mode 基础 Term mode 把证明写成一个表达式，该表达式的类型就是命题。Lean 4 的类型论里，命题是类型，证明是居民（inhabitant），“证明成立"等价于"该类型有居民”。 fun、⟨⟩、点投影 12345678-- 蕴含：函数抽象theorem impl_intro (A B : Prop)...

Lake 是 Lean 4 的官方构建系统与包管理器，随 lean 工具链一同分发。形式化方法系列的第 07-08 篇已覆盖 elan 安装与 lake new 起手骨架；本篇从那个骨架向前推进，聚焦生产级项目需要的部分：toolchain 锁定、Mathlib4 依赖引入、lake-manifest.json 版本固定、多目标 lakefile 设计，以及可直接套用的 GitHub Actions CI 配置。 lean-toolchain：锁定工具链版本 项目根目录的 lean-toolchain 是一行纯文本文件，内容就是 toolchain 字符串： 1leanprover/lean4:v4.12.0 elan 读取该文件，自动下载并激活对应版本的 lean 与 lake。项目目录内的所有 lake 命令都在该 toolchain 下执行，与机器全局版本无关。 版本字符串的两种合法格式： 格式 示例 说明 正式 release leanprover/lean4:v4.12.0 推荐生产项目使用 nightly leanprover/lean4:nigh...

图工程有两重含义。《深入图工程》讨论的是以图数据为中心的系统工程——图数据库、图计算引擎、知识图谱。本文讨论第二重：当 Coding Agent 系统本身成为一个图结构的工程制品时，传统图工程的哪些原理可以复用，哪些问题是全新的。 2024-2026 年间，Agent 系统从"一个 LLM 调用 + 几个工具"扩展到多步骤、多角色和可恢复执行。LangGraph 直接使用状态图；CrewAI 以 agents、tasks、crews 和 flows 为主要抽象；AutoGen 同时提供 conversation、team 与实验性的 GraphFlow。图适合作为统一分析视角，但不能把不同框架都改写成同一种图调度器。 Agent 系统中的三类图结构 Agent 系统至少包含三类不同性质的图，它们在生命周期、变化频率和工程约束上各不相同： 执行图（Execution Graph）：Agent 单次任务执行的控制流。每个节点是一个计算步骤（LLM 调用、工具执行、条件判断），边表示控制转移。LangGraph 的 StateGraph 是这一类的典型代表。执行图在...