oh-my-claudecode vs oh-my-openagent：两大 Agent 编排框架深度对比与实用教程
2026 年的 AI 编程工具生态中，单模型 CLI 已不再是终点。围绕 Claude Code 和 OpenCode 两大基座平台，不仅各自拥有原生的多 Agent 并行能力，还分别涌现出 oh-my-claudecode（OMC） 和 oh-my-openagent（OmO） 两个编排插件。 本文的 OmO 部分以 2026 年 8 月 13 日能够核验的稳定版 v4.19.4 为基线。GitHub 同期已经出现 v5.0.0-beta.7，但它仍是预发布版，不能拿来替代稳定版说明。 项目在 v3.11.0 更名为 oh-my-openagent，仓库也迁到了 code-yeongyu/oh-my-openagent。命名迁移尚未把所有历史痕迹抹平：v4.19.4 的 package.json 仍以 oh-my-opencode 发布，同时提供 oh-my-openagent、omo 等命令别名。文章统一用新品牌名 OmO；安装与诊断命令使用新别名，涉及包元数据时保留旧包名，避免把兼容期写成已经彻底结束。 TL;DR：日常命令选择指南 如果你只想知道"该用哪个命...
深入 Lean 03：Universe 与类型层级实战
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 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 模型...
深入 Lean 17：可执行代码与 FFI
Lean 4 同时承担定理证明器与通用程序设计语言两种角色。前十六篇聚焦逻辑与证明工程；本篇转向可执行端：从 #eval 求值，到 lake build 编译本地二进制，再到通过 FFI 调用 C/Rust 代码，最后讨论影响运行期性能的属性与编译选项。 Lean 4 作为编程语言：#eval 与 IO Lean 4 的类型论本身不区分"证明代码"与"程序代码"——两者都是项（term）。运行 Lean 代码最轻量的方式是 #eval，它在编译时对表达式求值并在 InfoView 中显示结果。 123#eval 1 + 1 -- InfoView 输出：2#eval "hello".length -- InfoView 输出：5#eval List.range 5 -- InfoView 输出：[0, 1, 2, 3, 4] 涉及副作用（文件读写、网络、标准输入输出）时，表达式类型变为 IO α： 12#eval IO.println "hello from Lean"-- 输...
深入 Lean 16：用 Aesop 写声明式自动化
手动证明每一步的好处是透明可控，坏处是重复劳动积累。Aesop（Automated Extensible Search for Obvious Proofs）是 Lean 4 / Mathlib4 的声明式自动化框架：用户注册规则集，Aesop 在目标上做有界搜索，自动完成"显而易见但手写繁琐"的证明。本篇覆盖 Aesop 的规则注册、优先级系统、safe/unsafe/norm 三类规则、自定义规则集，以及与 Coq 的 auto/eauto 的设计差异。 Aesop 的基本用法 12345678import Aesop-- 标记引理为 Aesop 规则@[aesop safe]theorem and_comm_aesop : ∀ (p q : Prop), p ∧ q → q ∧ p := fun _ _ ⟨hp, hq⟩ => ⟨hq, hp⟩example (h : A ∧ B) : B ∧ A := by aesop @[aesop safe] 把 and_comm_aesop 注册为安全规则。aesop tactic 在遇到形如 _ ∧ _...
深入 Lean 15：编写 elaborator 与 command
第 14 篇展示了 tactic 如何操作 MVarId 和 Expr。本篇向上走一层：elab 不仅能定义 tactic，还能定义 term elaborator 和顶层 command。三者共享同一套 Expr 构造工具，但触发时机和返回值语义不同。 elab 的三种角色 elab 关键字根据后缀决定 elaborator 类别： 123elab "my_tactic" : tactic => ... -- 操作目标列表，无返回值elab "my_term" : term => ... -- 返回一个 Expr（证明项或值）elab "my_command" : command => ... -- 顶层副作用，无返回值 三者的 monad 环境： 类别 Monad 核心职责 tactic TacticM 消费/产生 MVarId term TermElabM 返回 Expr，可能带约束 command CommandElabM 修改环境、输出消...
深入 Lean 14：元编程模型：Expr/MVarId/MetaM
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 ...
深入 Lean 13：有限组合与数论片段
Mathlib4 提供了一套完整的有限集合与大算子（BigOperators）机制，使得组合数学和初等数论的形式化证明可以在接近数学原文的符号层面进行。Finset 表示有限集合，Fintype 约束类型的有限性，BigOperators 引入求和与连乘的紧凑记号，Nat.Prime 与 Nat.factors 覆盖自然数素数理论的基本引理。本篇在此基础上，进一步介绍 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 val : M...
深入 Lean 12：拓扑与分析基础结构导览
Mathlib 的分析库以 Filter 为核心抽象，在此之上叠加拓扑、度量和赋范结构，统一表达极限、连续、收敛等概念。理解这套分层设计，是读懂 Mathlib 分析证明的前提。本篇梳理 Filter、TopologicalSpace、MetricSpace 和 NormedSpace 四层结构的定义方式和证明惯用法，并通过具体可运行代码展示各层之间的关联。 前置阅读：本系列 09 Mathlib 搜索技巧、10 类型类层次、11 在 Mathlib 上证一个小定理。 Filter：分析库的基础抽象 为什么不直接用 ε-δ 经典分析教材用 ε-δ 定义极限：对每个 ε > 0，存在 δ > 0，使得……这个定义能精确刻画单个极限，但在证明库里它有两个缺陷。第一，同一个"极限"概念在不同情形（趋向实数点、趋向无穷、序列极限、网极限）下需要写出形状不同的 ε-δ 公式，导致同一条定理（如极限的线性性）在每种情形下各需一个版本。第二，组合两个极限结论时，条件匹配需要手动传递 ε/2 技巧，证明文本冗长。 Mathlib 选择用 Filter 把&quo...
深入 Lean 11：在 Mathlib 上证一个小定理
向 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 确实...