Optimal Play in Caverna: A Formal Proof of Weak Dominance

Overview. We present a complete formal proof that the furnishing rush strategy is the unique weakly dominant pure strategy in 2-player Caverna (the Cave Farmers European board game by Uwe Rosenberg). The argument proceeds bottom-up: we first formalize the game’s scoring system, resource economy, and 48 furnishing tiles, then analyze eight candidate strategy archetypes through an \(8 \times 8\) payoff matrix, and finally establish weak dominance, Nash equilibrium uniqueness, and the price of anarchy.

Formalized in Lean 4 with Mathlib.

Author. Stephen Diehl.