Tic-Tac-Toe
Fully solvedThe explicit reachable transition system, quotiented by the board’s geometric symmetry and solved by backward induction: perfect play is a forced draw.
Read more »Games
Learning perfect play for board and card games by treating each one as a verification problem: if you can enumerate the reachable state space exactly, you can model-check properties of it, synthesise optimal strategies, and compute exact game values — with proof, not approximation.
Each game below is studied at its minimum player count and gets its own write-up: the rules, the formal model (transition system, MDP, POMDP or extensive-form game), the solving technique, and the certified results. Every write-up is playable in the browser: the verified strategy runs live on the page.
- Fully solved the stated results carry a machine-checked proof.
Nim
Fully solvedThe canonical impartial combinatorial game: the first player wins iff the nim-sum is non-zero — the Sprague–Grundy / Bouton criterion, machine-checked with z3.
Read more »Pig
Fully solvedThe dice game as a Markov decision process solved by value iteration: the first player wins 53.06% under optimal play, certified at the Bellman fixpoint.
Read more »