Formally Verifying PBS Kids with Lean4
Summary
A detailed walkthrough of using Lean4 to formally verify a PBS Kids Cyberchase Nim-like puzzle. The post covers modeling the game, defining a strategy, handling mutual recursion termination, and proving correctness with Lean tactics like rw, simp, and omega, along with reflections on autoformalization and future work.