守株阁

题面 把一个真实落地的项目折叠成一道架构题： 有一个 git 仓库，里面散落着 N 个 SKILL.md 文件（带 YAML frontmatter + 同目录的资源文件）。要做一个内部「Skill Hub」服务： 浏览、搜索、分类、查看详情 在线预览 markdown 与文件树 一键下载某个 skill 的 zip 包 源仓库 push 时 Hub 要自动跟上 部署形态是单 Node 进程（容器平台只给一个端口） 怎么设计？ 约束是分批给的。每听完一版方案，就追加一个新约束逼着方案迭代。下面 14 层按这个节奏走。每层先写最朴素的版本，再写暴露出来的问题，最后写改进，配最小可读的代码片段。 代码片段、字段名、目录名都是从一个真实落地的项目里抽出来的，业务和组织信息已经全部抹掉。 第 1 层：最朴素的版本 最直接的实现： 12345app.get("/api/skills", async () => { await exec("git clone --depth 1 $REPO /tmp/work"); con...

到第 08 篇为止，"编译通过 = 定理得证"的等式在 Lean 4 里已经成为肌肉记忆。但每个写过证明的读者迟早会问： 我相信 Lean 编译通过等价于定理得证。但这条信任传到底是信什么？ 本篇专门回答这个问题。形式化方法不让人脱离信任，它让人把"信什么"明确化。明确化的边界叫可信计算基底（Trusted Computing Base，TCB）。形式化系统的 TCB 越小越好；任何 sorry、任何坏公理、任何元理论缺口都会让 TCB 撑大。 本篇按"哪些东西必须信、哪些东西不必信、信任面破口长什么样、坏公理怎样让整套系统崩"四段展开。 什么是 TCB TCB 在安全领域指"必须正确才能保证系统安全的最小组件集合"。在形式化系统里它有一个对位的定义： 必须正确才能让"编译通过 = 定理得证"这条等式成立的最小组件集合。 对一个用 Lean 4 写出的证明，TCB 通常包括： Lean 4 的类型检查器内核——按规则机械验证每一段良类型项。 Lean 4 内核所依赖的底...

第 07 篇把 Lean 4 环境装好了。本篇真在 Lean 4 里写一组经典命题的完整证明：合取交换律、析取交换律、等价、自然数加法交换律、列表拼接长度。每条命题给出 term mode 与 tactic mode 两种写法。 读完本篇之后，"在 Lean 4 中写一段非平凡证明"对读者来说不再是抽象。系列的主线问题"为什么编译通过就是定理得证"也由这些可在 InfoView 里看到 No goals 的具体证明落到肌肉记忆。 推荐的最小工程结构 把本篇所有代码放进 FormalIntro/First_Theorems.lean： 123456namespace FormalIntro.First-- 后面的代码都在这里-- ...end FormalIntro.First 每条命题都写两遍：term mode 优先，tactic mode 对照。看到等价的两种形态可以加深"tactic 是构造项的元程序"这条直觉。 命题逻辑 合取交换律 12345678-- term modetheorem and_comm_t ...

到第 06 篇为止，本系列的所有概念都已铺开。从本篇开始换姿势：不再用 Python 模拟，也不再贴 Lean 4 片段当示意，而是让读者在自己机器上跑 Lean 4，写下第一个证明，看着编辑器右栏的 No goals 出现。 本篇是一篇短工具文：装 elan、跑 lake new、配 VS Code、写一段会动的 Lean 代码。系列从下一篇开始所有 Lean 示例都默认在这套环境里跑。 一句话总结要装什么 组件 作用 安装方式 elan Lean 4 版本管理器（类似 Rust 的 rustup） 官方脚本一行 lean Lean 4 编译器与类型检查器 elan 自动拉 lake 项目与依赖管理器（类似 cargo） 随 lean 一起 VS Code + Lean 4 插件 编辑器 + InfoView 应用商店搜 lean4 完全不想装本地环境的读者，可以直接用 Lean 官方 Web 编辑器 https://live.lean-lang.org/。本篇先讲本地路径，最后留 Web 编辑器的最小回退方案。 安装 elan elan 是 ...

第 05 篇把 STLC 升级到带 Π 与 Σ 的依值类型，量词被纳入类型系统。但要在自然数、列表、树这些数据结构上证明命题，还差一件事：归纳法。 直觉上，“自然数加法可交换"这种命题的证明依赖"对所有自然数都成立”，而自然数本身是一个归纳定义的对象。要让证明跟着数据结构走，类型系统需要支持归纳类型：用一组构造子定义一族数据，然后允许"按构造子分情况讨论"——模式匹配——作为消去规则。 本篇说清楚归纳类型怎样定义、模式匹配怎样替代逻辑里的归纳推理、为什么"归纳法"在依值类型系统里就是"良基递归"。 inductive：用构造子定义一族数据 自然数在 Lean 4 里是这样定义的： 123inductive Nat where | zero : Nat | succ : Nat → Nat 这条 inductive 声明在做四件事： 引入一个新类型 Nat。 声明两条构造子：zero 与 succ。 自动生成一组消去规则：可以对 Nat 做模式匹配。 自动生成一条递归子（recursor）Nat...

到第 04 篇为止，STLC 已经把直觉主义命题逻辑全部装进类型系统。但日常数学和工程里大量命题超出命题逻辑范围：“对任意自然数 n，n + 0 = n”、“对任意列表 xs，reverse (reverse xs) = xs”。这些命题都带量词，命题逻辑写不出来。 让类型系统能表达量词的关键扩展叫依值类型（dependent types）：允许类型本身依赖值。一旦允许类型依赖值，∀ x : A, P(x) 就能翻译成"对每个 x : A 都给出 P(x) : Prop 的函数"——这条函数本身有依值的返回类型。 本篇说清楚依值函数 Π、依值积 Σ、Vec n α 这种经典例子，并把它们与一阶逻辑的 ∀、∃ 精确对应起来。 STLC 卡在哪里 STLC 里函数类型形如 τ1 → τ2，τ2 必须是与 τ1 完全无关的、固定的类型。例如可以写： 1length : List Nat → Nat 但写不出： 1replicate : (n : Nat) → Vec n Nat 后者的返回类型 Vec n Nat 依赖输入 n。STLC 的 → 不允许这件事。 类...

上一篇给出了 STLC 的类型规则。规则本身只描述了"什么样的程序合法"，并没有说"怎样判断合法"。本篇把这个判断过程写成一段可运行的 Python 程序，约 200 行。 读完这段代码之后，"类型检查 = 证明检查"会从概念对位落到一段能跑出真实输出的事实。系列主线问题"为什么编译通过就是定理得证"的第一层——证明可被机械检查——也在这里被实证。 算法策略：从规则到代码 上一篇的规则形如： 123 Γ ⊢ e1 : τ1 → τ2 Γ ⊢ e2 : τ1────────────────────────────────────── (App) Γ ⊢ e1 e2 : τ2 把这条规则直接读成一段 Python 代码： 12345678def synth_app(env, app_expr): fn_ty = synth(env, app_expr.fn) if not isinstance(fn_ty, Arrow): raise TypeE...

上一篇打通了命题与类型的对应：命题就是类型，证明就是程序。本篇把这条同构落在最小可证明系统上——简单类型 lambda 演算（Simply Typed Lambda Calculus，STLC）。 STLC 是类型系统的"hello world"。它语法只有三种表达式、五条核心类型规则，却已经能精确对应整个直觉主义命题逻辑。读懂 STLC 之后，依值类型、归纳类型、Lean 4 都只是在它上面加构造，不会改变骨架。 本篇先写出 STLC 的语法和类型规则，再画一棵推导树，最后说清楚 STLC 能证明什么、不能证明什么。下一篇把这些规则用 Python 落地成一个真跑的类型检查器。 三种表达式 + 三种类型 STLC 的核心语法可以用 BNF 写成： 123456e ::= x -- 变量 | λ x : τ . e -- 函数（抽象） | e1 e2 -- 调用（应用）τ ::= A -- 基本类型 | τ1 → τ2 ...

上一篇用 BHK 解释把"证明"重新定义成"构造一个见证物"，并提到那份翻译表"看起来就是一组类型"。本篇正式给出这个直觉的精确版本：Curry-Howard 同构——命题就是类型，证明就是程序，证明检查就是类型检查。 这条同构是形式化方法的基石。理解了它，"为什么形式化编译器编译通过就是定理得证"这条主线问题第一层翻译就被打通：检查证明这件事被压成了机械的类型检查。 本篇不假设读者会 Coq 或 Agda，但要求理解上一篇的 BHK 表，并能读简单的 Python 类型注解。中段会用 Lean 4 写两段简短代码做对照。 同构的对照表 把上一篇 BHK 表整理成"逻辑端 ↔ 类型端"的并列形式： 逻辑端 类型端 程序端的项构造 程序端的项消费 原子命题 A 基本类型 A 公理/假设变量 当作变量使用 ⊥ 空类型 Void / Empty 没有构造子 absurd : Void → C ⊤ 单位类型 Unit () 无信息可消费 P ∧ Q 积类型 P ...

形式化方法导引系列的主线问题是：“为什么编译通过就是定理得证”。要把这条等式撑起来，第一步是回答一个看似更基本的问题：什么算一个证明。 中学数学里"证明"通常意味着一段以"证："开头、以"证毕"结束的自然语言论证。这种证明里允许使用反证法、双否定消去、排中律，论证的合法性靠人类同行评议把关。这条路线下，"证明"是一份可被阅读和判断的文档。 形式化系统走另一条路。证明被要求成为一个可以被机械构造、机械检查的对象。这条要求一旦贯彻到底，传统数学里的"反证"和"排中"会被部分剥离，剩下一种叫直觉主义逻辑或构造主义逻辑的子系统。BHK 解释（Brouwer-Heyting-Kolmogorov）正是把"证明"在这个子系统里重新定义成"构造一个见证物"的规范。 本篇展开 BHK 翻译表，解释为什么它天然导向 Curry-Howard 同构，并用 Python 把表里的每一条编码成一个数据类。 古典逻辑与直觉主义逻辑的分歧 考虑一条...