Onitama · Sato 2014 · selected finite-model records 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 available to your opponent after the intervening exchange. That cycling is a central strategic mechanism. The board has twenty-five squares; its size alone says nothing about how difficult the game is to solve.
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'
Within the displayed GameState/Step model, every modeled state has a successor because the pass transition rotates a card when no piece move is available. This is a statement about that formal transition relation.
pieceCount initialBoard = 10
The displayed initialBoard definition has pieceCount 10. The page's phase labels key off this modeled count; the record makes no broader game-solving claim.
Act 2— Cards
Sixteen movement patterns
In the modeled base catalogue, each card carries between two and four offsets — candidate displacements 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 are listed in this modeled base catalogue. Each lists between two and four offsets. The linked record Audrey.Onitama.Catalog.all_length states the list length; all_offset_counts states the per-card offset-count interval for that list.
∀ (c : Card), c ∈ all → ∀ (o : Int × Int), o ∈ c.redOffsets → -2 ≤ o.1 ∧ o.1 ≤ 2 ∧ -2 ≤ o.2 ∧ o.2 ≤ 2
For each card in the modeled base-card catalogue, every listed red-perspective offset lies between -2 and 2 on both coordinates. This bounds offsets; board-edge legality is checked separately.
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. After the opponent’s intervening exchange it enters their hand and can be used on their following turn.
That exchange is the core tempo structure modeled here. Every move also passes a card through the side slot. Choosingwhich card to discard is one strategic lever alongside choosing which piece and destination to play. 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.
In this fixed sequence, each label has occupied the side slot at least once (C starts there). A played card enters the opponent’s hand after their intervening exchange and can be used on their following turn. Actual card choices produce different sequences; this widget is not a search or strategy proof.
∀ (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 modeled win predicates
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 formal model can evaluate. These receipts concern the named predicates and witness states, not a solution of the full game.
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
Under the displayed winner hypothesis and this value definition, every search depth returns winValue. This is an absorbing-terminal lemma, not a result that search reaches such a state.
∃ 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
A coarse finite configuration envelope
The type Board = Fin 5 → Fin 5 → Option Piece has exactly 5 ^ 25 inhabitants: each square independently holds one of four piece labels or is empty. Most of those boards violate game constraints. A deliberately loose configuration envelope then uses five ordered card slots with at most sixteen choices each and two players to move: 5^25 · 16^5 · 2. It overcounts duplicate cards, impossible piece inventories, and unreachable histories.
The comparison record checks that this coarse numeral is below a separately pinned 10^46 chess estimate. It does not count legal Onitama states, bound the reachable state graph, prove tractable search or human solvability, or establish an eight-ply solution. Finiteness and a smaller envelope are not algorithms.
Fintype.card Board = 5 ^ 25
Exact for the unconstrained Board function type: each of 25 squares independently has five contents. It is not the cardinality of legal or reachable boards.
rawOnitamaEncodingCount < chessStateEst
A numerical comparison between the defined loose envelope and the defined chess estimate. It inherits both definitions' assumptions and proves no search-complexity or solvability claim.
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 much of the depth appears to come from cycling: every card played moves through the shared side slot. Published solver work studies that search behavior, but the finite-card and board receipts shown here do not reproduce those empirical results. The Lean formalisation pins down selected transition invariants and coarse envelopes; strategic difficulty remains a separate question.
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).