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 »Knight’s Tour
Fully solvedThe oldest puzzle here: a knight visiting every square exactly once — a Hamiltonian path in the knight graph. Existence is settled exactly to 8 × 8, and an exact oracle flags the legal moves that quietly make a tour impossible.
Read more »Games I recommend
The games above are here because they can be proved things about. Separately, I keep a list on BoardGameGeek of board games I simply enjoy playing — recommendations rather than results.