Onitama · Sato 2014 · kernel-checked in Lean 4
Onitama
Five squares each way, sixteen cards, one tempo invariant.
A 5×5 abstract perfect-information game. Each player holds two cards from a hand of sixteen; a fifth card waits at the side. Every move plays a card and trades it for the side card — so the card you spend becomes your opponent’s in two turns. That is the entire strategic engine. The board has only twenty-five squares; the depth is in the cycling.
Act 1— Board
Twenty-five squares, ten pieces
Two rows of five pieces face each other across an empty middle. Each side has a Master in the centre column — on the Temple Arch— and four Students flanking. The Masters are the kings; the Students are the pawns. Win by capturing the opposing Master, or by walking your own Master onto the opponent’s Arch.
∀ (s : GameState), ∃ (s' : GameState), Step s s'
Every state has at least one legal successor: if no piece can move, the player passes by rotating a card. Tempo is always forced; Onitama cannot end in stalemate-loss.
pieceCount initialBoard = 10
Ten pieces at the start, kernel-checked. The phase classification (Opening / Middlegame / Endgame) keys off this count.
Act 2— Cards
Sixteen movement patterns
Every card carries between two and four offsets — the squares the card’s owner may move a piece to, measured from the piece’s current square. Offsets are written from Red’s perspective; Blue negates each component. Tiger jumps two squares forward or one square back; Dragon spreads diagonally; Frog hops sideways and forward at once. Click a card to compare both sides.
- (+0, +2)
- (+0, -1)
- (+0, -2)
- (+0, +1)
Sixteen cards in the base game. Each lists between two and four offsets. The Lean theorem Audrey.Onitama.Catalog.all_length certifies the deck size; all_offset_counts certifies the offset-range bound.
∀ (c : Card), c ∈ all → ∀ (o : Int × Int), o ∈ c.redOffsets → -2 ≤ o.1 ∧ o.1 ≤ 2 ∧ -2 ≤ o.2 ∧ o.2 ≤ 2
Every base-card offset lies inside a 5 × 5 window. No card can teleport; all move patterns fit in a single board's worth of distance.
Act 3— Tempo
The card you spend is the card you give away
Five card slots: two in Red’s hand, two in Blue’s, one at the side. The side card belongs to nobody and waits. When you play one of your two cards, you move a piece using its offsets, then you swap the played card with the side card. Two turns from now your opponent will have access to the card you just used.
That is the entire tempo structure of the game. Every move is also a gift. Choosing which card to discard — not which piece to move — is the strategic lever. A Tiger in your hand is two squares of forward power for you; a Tiger you played last turn becomes two squares of forward power for the opponent.
After turn 4 every card has visited the side at least once. The card you play is the card your opponent picks up two turns later — every move is also a gift.
∀ (s : GameState), (applyPass (applyPass s)).toMove = s.toMove
Two consecutive passes return the turn marker to the original player — the cycling structure has period dividing 2 on the toMove field, even when nobody captures.
Act 4— Endgames
Two ways to win, kernel-checked
The rulebook gives two victory conditions: Way of the Stone (capture the opposing Master) and Way of the Stream(move your own Master onto the opponent’s Temple Arch). Both are formalised as concrete game states the kernel can evaluate.
winner redWonState = some Player.red
A board with only Red's Master remaining — Blue has no Master, so Red has won. Computed, not assumed.
∀ (s : GameState), winner s = some Player.red → ∀ n, value n s = winValue
Once Red wins, the negamax value at every depth is exactly winValue. Won states are absorbing — the search tree below them collapses to the leaf heuristic.
∃ s_r s_b : GameState, winner s_r = some Player.red ∧ winner s_b = some Player.blue
Onitama is not a one-sided game — both colours admit winning states. Closed by exhibiting concrete witnesses on each side.
Act 5— Numbers
Twenty-five orders of magnitude smaller than chess
Onitama’s state space is Fintype.card Board = 5 ^ 25 ≈ 3 × 10¹⁷ board configurations, multiplied by sixteen choose five card placements — loosely 5^25 · 16C5 · 2 ≈ 4.7 × 10²¹. Compare to the standard chess legal-position estimate of about 10⁴⁶. Twenty-five orders of magnitude is the gap between a game humans solve in a coffee break with an 8-deep minimax and a game machines have not solved yet.
Fintype.card Board = 5 ^ 25
Each of 25 squares is either empty or holds one of four piece types (Red Master, Red Student, Blue Master, Blue Student) — five contents per square. Pi.fintype + Fintype.card_fun closes it.
looseStateBound * 10 ^ 25 ≤ chessLegalPositions
Even the loose state-space bound for Onitama, scaled up by 10²⁵, still fits inside chess's standard legal-position estimate. The gap is real.
Coda
A small game with a long tail
Onitama looks like a five-minute exercise. The board is small, the cards are simple, the win conditions fit on a coaster. Empirically the depth comes from the cycling: every card you play you also lend out, and the lender is always two turns ahead of the borrower. Saffidine, Jouandeau, and Cazenave (ICGA Journal, 2018) report that even strong human players miss tempo three-cycles regularly. The Lean formalisation pins down what the cycling does to the state space; what it does to a game is still mostly empirical.
Audrey.Onitama sits next to Audrey.Signal — both are deduction-and-search games where the strategic content lives in a small finite catalogue and a deterministic cycling rule. Same shape, different dressing.
References.
Sato, S. Onitama. Arcane Wonders, 2014. Rulebook and base-card deck.
Saffidine, A.; Jouandeau, N.; Cazenave, T. Solving Onitama. ICGA Journal 40(4), 305–317 (2018).