The Square Achievement Game on n × n Boards

Two players take turns claiming cells of an $n \times n$ grid. The first to hold all four corners of an axis-parallel square wins; a full board with no square is a draw. Erickson asked who wins. The first player wins exactly when $n \ge 5$ , and from 6 × 6 up a rule of one paragraph wins, with no lookup table. The whole argument, every board size at once, is checked in Lean 4.

Theorem. In the square achievement game on the

n \times n

board, the first player has a winning strategy if and only if

n \ge 5

. For

n \le 4

the game is drawn under optimal play: each player can secure at least a draw. For every

n \ge 6

, the first player following the plus rule wins.

The rule, for every board from 6 × 6 up:

Open at (2,2). Answer the first reply at (3,2), except against seven first replies near the opening, where a small diagram in the paper gives the second move.
If some empty cell completes a square of the first player, play it. Otherwise, if some empty cell completes a square of the second player, block it.
Otherwise follow the line chosen after the second reply: at most three tempo moves, single forcing moves each answered by a forced block, and then the arms of a plus.

The plus, in three pictures. Left, the first player holds the centre (2,2) and one arm (3,2); the other arms are a, the diagonals d. Middle, playing an arm perpendicular to the held one makes three corners of a small square, so the second player must block on the diagonal, dashed. Right, after two such arms, the last arm threatens two diagonals at once, and no single block stops both. When the second player holds an arm or a diagonal, the rule first plays up to three tempo moves, each answered by a forced block, to place the stones it needs.

The rule reads only its own stones, the second player's stones inside the 17 × 17 base board, and one derived cell, the hidden corner, so one rule serves every board, and it plays the same 79 lines on every board from 6 × 6 to 17 × 17. Against a second player who always blocks every line ends by ply 17; that bound is computed from the lines and is not part of the formal theorem. On 5 × 5 no purely forcing strategy from (2,2) exists, and a table with quiet moves at branch points plays instead.

Play against the rule. The bot moves first, explains each move, and draws the line it is following; click a cell, or use the arrow keys and Enter. Change n to explore: on 5 × 5 the table plays, and below 5 × 5 neither side can force a win.

What you have to trust

The headline statements in the development read as follows, with P1CanWin the first player forcing a win, the two draw predicates each player securing at least a draw, and WinsWith σ n h the tree in which the first player plays the move of the strategy σ at every node after the history h, against every legal reply, ending in a first-player square on every branch.

theorem outcome (n : ℕ) :
    (P1CanWin n ∅ ∅ ↔ 5 ≤ n) ∧
      ((P1CanDraw n ∅ ∅ ∧ P2CanDraw n ∅ ∅) ↔ n ≤ 4)

theorem plus_wins_with {n : ℕ} (h : 6 ≤ n) :
    WinsWith plusMove n []

The definitions behind them, cells, squares, the winning predicate as a strategy tree, and the 250 lines of plusMove, are the only part a skeptic has to read. Beyond them the trust is Lean's kernel, mathlib, and native_decide, which lets the Lean compiler evaluate the exhaustive checks instead of the kernel. The 5 × 5 table was found by a Python search, but nothing about that search enters the proof, since a wrong table fails the check. The bot on this page is a TypeScript copy of the rule. The site's tests replay it against the lines the Python implementation commits to on every reply pair of the 6 × 6 board and on the anchored positions of the proof, and the paper reports that those lines agree with the Lean definition.

Open questions

The rule wins by ply 17, a bound computed from its lines. How quickly can the first player force a win on the $n \times n$ board, and can one rule of comparable length be fastest for every $n$ ? The rule's second move has seven exceptions; is there an opening that needs none? The 6 × 6 region and the 17 × 17 base board are least in the senses the paper makes precise, but whether a rule can read less than the second player's stones inside the base board is open. And 5 × 5, where no purely forcing strategy from (2,2) exists, still has no short rule.