Optimal Play in Caverna

A formal proof that the furnishing rush strategy is the unique weakly dominant pure strategy in 2-player Caverna (the board game by Uwe Rosenberg), verified in Lean 4 with Mathlib.

This is a fun hobby project that I haven't independently verified; I'm just putting it online for fun, so please don't take it too seriously, it's a board game after all.

Blueprint Source Code

Core Theorem (Weak Dominance). For all opponents and all alternative strategies, the furnishing rush payoff is at least as large, and strictly larger for at least one opponent. The unique pure Nash equilibrium is the furnishing rush mirror match.

The formalization is complete