Formal proof that furnishing rush is the unique weakly dominant strategy in 2-player Caverna.
# lean
brew install elan-init
elan toolchain install leanprover/lean4:v4.28.0
# blueprint deps
brew install graphviz
curl -LsSf https://astral.sh/uv/install.sh | sh
uv tool install leanblueprint
lake exe cache get # fetch mathlib cache (~5 min first time)
lake build # build project
leanblueprint web # compile HTML + dependency graph
leanblueprint serve # http://localhost:8000
lake exe checkdecls blueprint/lean_decls