Stephen Diehl 用 Lean 4 形式化验证了整个 Caverna 桌游，证明 furnishing rush 是唯一的最优策略。这是一个极端但精彩的形式化方法应用案例。

🎮 项目概览

🏗️ 技术方法：标签转换系统 (LTS)

标签转换系统是一个三元组 (S, A, T)：

• S - 状态集合
• A - 动作集合
• T ⊆ S × A × S - 转换关系

在 Lean 4 中，LTS 定义为：

structure LTS (State : Type) (Action : Type) where
  init : State -> Prop
  trans : State -> Action -> State -> Prop

可达性证明

Reachability 是一个归纳类型：

inductive Reachable (sys : LTS State Action) : State -> Prop where
  | init : forall s, sys.init s -> Reachable sys s
  | step : forall s a s', Reachable sys s -> sys.trans s a s' -> Reachable sys s'

这比测试更强。测试检查特定的玩牌序列。不变式证明覆盖每一种可能的合法移动序列，包括人类永远不会玩的序列。

📐 游戏建模

完整的游戏状态

structure GState where
  round : Nat
  phase : Phase
  p1 : FullPlayer
  p2 : FullPlayer
  p1IsFirst : Bool
  placementsLeft : Nat
  acc : AccState
  occupiedSpaces : List ActionSpaceId := []
  harvestSchedule : Nat -> HarvestEvent
  wishIsUrgent : Bool := false

转换关系

转换关系是一个单一函数，对 (phase, act) 进行匹配。每个 case 都是一条游戏规则。最后一行很美：

| _, _ => False

这意味着：任何未明确列出的动作都是非法的。转换关系是封闭的。没有未定义行为，没有边缘情况，没有"规则没说我不能"。如果不在 match 中，就不会发生。

🎯 核心结论：Furnishing Rush 是最优策略

游戏时间线

• 12 轮游戏
• 第 4 轮 "Wish for Children" 允许第一次家庭成长（2 → 3 矮人）
• 第 8 轮 "Family Life" 允许第二次家庭成长（3 → 5）

关键洞察

没有成长：44 次矮人放置
一次成长（第4轮）：47 次
两次成长：56 次

从"不成长"到"两次成长"的 27% 差距是游戏中最主要的策略杠杆。

🔬 依赖类型的妙用：让非法状态不可构造

用依赖类型让非法游戏状态无法构造。武器是最清晰的例子：

structure Weapon where
  strength : Nat
  h__min : strength >= 1
  h__max : strength <= 14

每个 Weapon 值都带有其强度在范围内的证明。这意味着 forgeWeapon 必须产生证据证明它返回的值是有效的。

🔗 资源链接

• 交互式证明蓝图
• 源代码 (GitHub)

💡 启示

"My friends think this is excessive. My friends also lose at Caverna."

这是一个极端但精彩的形式化方法应用案例，展示了：

• 有限确定性完美信息游戏可以用形式化方法分析
• Lean 4 的依赖类型系统非常适合建模游戏规则
• 不变式证明可以覆盖测试无法覆盖的边缘情况
• 形式化方法不只是用于关键系统，也可以用于有趣的问题