Summary. Two players alternately claim cells of an grid; the first to hold all four corners of an axis-parallel square wins, and a full board without one is a draw. The first player has a winning strategy if and only if . For one strategy serves every board: a rule with no lookup table whose moves after the second reply are all forcing, built around the plus, a stone with the four cells at a common distance from it along the axes, a shape proposed for this game by Sirgedas in 2010. The rule is checked on the boards from 6 × 6 to 17 × 17, a simulation theorem carries one checked run on the 23 × 23 board to every larger board, and the proofs are formalized in Lean 4. This guide follows the paper section by section, with the proofs left out.
Two players alternately claim empty cells of an grid, the first player moving first. A player wins upon holding all four corners of a square with horizontal and vertical sides, of any size: the cells for some . If the board fills with no player holding such a square, the game is a draw. The case is allowed, so the smallest winning shape is a 2 × 2 block; tilted squares do not count.
Erickson posed the game and asked for the outcome under optimal play [2], and the question is recorded on the Open Problem Garden [3] and on MathOverflow [12]. It is an achievement game in the sense of Harary [1]: both players pursue the same goal, and a player who loses the race may still secure a draw. The convention goes back to the positional games of Hales and Jewett [8]; a recent unified treatment of achievement conventions is by Galliot and Sénizergues [10], and the general theory of positional games is in Beck [11]. Two boundary results were known. Jenrich reported computer searches showing that the second player can secure a draw on 3 × 3 and 4 × 4 and that the first player can force a win on 5 × 5 [4]. Bacher and Eliahou proved that every two-coloring of the 15 × 15 grid contains four equal-colored cells at the corners of an axis-parallel square, and that 15 is least with this property [5]; since no completed game on a board of size 15 or more is square-free, strategy stealing and determinacy give the first player a win there, though they produce no strategy. Between these results nothing was published, and no coloring argument can reach the boards from 6 × 6 to 14 × 14, since Bacher and Eliahou also exhibit square-free two-colorings of the 14 × 14 board. One idea had been sketched: answering Erickson's question on MathOverflow in 2010, Sirgedas proposed that the first player open in the centre and win by making a cross, a stone with its four neighbours at a common distance along the axes, each arm forcing a reply [13]; he noted that the cross can also be built on two stones in a row or column at distance two, worked out three of the nine first replies on the 7 × 7 board up to symmetry, and guessed that 5 × 5 was a draw. Concurrently with this work, Adler announced computer searches settling those nine sizes as first-player wins, with full strategy trees certified for 6 × 6 and 7 × 7 and search verdicts for the rest, cross-checked by independent runs at the smaller sizes [9]. What is new here is a single strategy that wins every board from 6 × 6 up, stated in a paragraph, and a proof checked by a proof assistant. The bot in Figure 1 plays that strategy.
The rule is built around one shape, the plus, which is Sirgedas's cross: the arms of a plus force the second player's replies one at a time, and the last arm threatens two squares at once. The sketch of 2010 covered one board and a few replies and did not say which plus to aim for, how to prepare one when the replies obstruct it, or why one board's analysis should carry to another; the rule settles the first two by a search with a fixed preference order, and the simulation theorem settles the third. The theorem for the rule is proved by checking the rule's forced tree on every board from 6 to 17 and by a simulation theorem, stated for any strategy, that carries a checked run on the 23 × 23 board to every larger board. The outcome theorem follows with an exhaustive refutation for and a strategy table for , whose play from the opening (2,2) is not purely forcing. Everything is formalized in Lean 4 [6] on mathlib [7], and the formal theorem for the rule states that the tree of the rule's own moves is winning, not only that a winning tree exists. The rule was extracted from an earlier lookup-table strategy, almost all of whose forcing plans were arms of a side-1 plus at (2,2) or (3,2), the rest preparing the side-2 plus at (3,2).
Cells are pairs , row then column, with row 0 at the top and column 0 at the left in the figures. The first player threatens at an empty cell if that cell together with three of the first player's stones is a square; the second player blocks by playing it. A move that makes exactly one threat is forcing; a move that makes two threats wins, since one block leaves the other. One move of either player is a ply, so the first player moves at the odd plies. The rule plays inside the region, the 6 × 6 corner of the board, and reads the second player's stones inside the base board, the 17 × 17 corner.
A plus of side at a centre cell has four arms, the cells at distance above, below, left, and right of the centre, and four diagonals, the cells at distance in both directions. Two arms are perpendicular if one is above or below the centre and the other to its left or right; the diagonal between them is the cell in the row of one and the column of the other. The centre, two perpendicular arms, and the diagonal between them are the four corners of a square of side . The region holds sixteen pluses of side 1 and four of side 2; side 3 does not fit.
Suppose the first player holds the centre and one arm of a plus, and the second player holds none of its arms and none of its diagonals. Playing an arm perpendicular to the held arm threatens at the diagonal between them, so the second player must block there or lose. Once the first player also holds the arm opposite the held one, the remaining arm is perpendicular to both and threatens at two diagonals at once, which no single block answers. So from a centre and one arm the first player reaches a double threat in three moves against a second player who has no threat and whose blocks make none. The opening (2,2) and the second move (3,2) are the centre and an arm of the side-1 plus at (2,2), and an arm and the centre of the side-1 plus at (3,2).
The rule's stones never leave the region, and the second player's stones in a position the rule reaches are two free replies and forced blocks, the blocks in the region as well. Two distinct corners of a square that both lie in the region confine the square to the 12 × 12 corner of the board. Hence a second-player stone beyond the base board shares no square with two blocks, and a second-player square through such a stone and a block has the two free replies as its other corners. That block is the one cell through which stones beyond the base board can affect the game.
Let and be two cells each having a coordinate at least 12. Their hidden corner is a cell of the region that together with and makes three corners of one square. Two cells have at most one hidden corner. The abstraction of a position consists of the first player's stones, the second player's stones inside the base board, and, once the second player has two stones, the hidden corner of the first two, if they have one. A second player forced to block at the hidden corner would hold three corners of that square and threaten at its fourth, a cell the rule does not read. So the rule never makes a threat whose only block is the hidden corner. It applies the restriction whenever the pair has a hidden corner, even when the square through it lies inside the base board and the restriction is not needed. The threshold 12 and the base 17 are tied by 17 = 12 + 5: a square through a region cell leaves the base board only if its side is at least 12. With a threshold of 11 and base 16 the argument would still work, and 11 is the least threshold for which a pair has at most one hidden corner; the rule has been checked only with base 17.
When no plus can be completed directly, because the second player holds an arm or a diagonal or because the arms would not force, the rule first plays moves that each force a block and so add a stone. In a position where the second player has no threat, a tempo move is a cell in the region that makes exactly one threat, such that the threat cell is not the hidden corner and after the block the second player still has no threat. A line from a position consists of some tempo moves, each followed by its block, and then the arms the first player does not yet hold of one plus in the region whose centre the first player holds, in some order, such that each arm before the last makes exactly one threat whose block is not the hidden corner, the last arm makes at least two threats, and the second player never has a threat. The key of a line is (number of tempo moves, number of arms to play, side of the plus, centre of the plus). The rule prefers the smallest key in lexicographic order, cells ordered by row and then by column, then the line its search generates first. It searches for lines with at most three tempo moves. Whether a line exists, and which is preferred, depends only on the abstraction of the position.
The move function has five clauses, tried in order. If some empty cell completes a square of the first player, play the least such cell. Otherwise, if some empty cell completes a square of the second player, play the least such cell. Otherwise, if the first player has no stone, play (2,2). Otherwise, if the first player does not yet hold the second move, play it: (3,2) against every first reply except seven cells of the region, for which the paper gives the move in a small diagram. Otherwise play the first cell the first player does not hold of the line chosen, once, from the abstraction after the second reply. The seven exceptions are exactly the first replies from which (3,2) fails; they were found by search. If the search returns no line the rule is undefined, and the checker of the verification section certifies that this never happens at a position the rule reaches.
The paper lists two complete games against a second player who always blocks. In the first the replies (0,0) and (4,4) are away from the opening pair and the basic line of Figure 3 wins at once, key (0, 3, 1, (2,2)). In the second the reply (3,1) is a diagonal of both side-1 pluses, no line with fewer than two tempo moves exists, and the line has key (2, 4, 2, (3,2)): two tempo moves and then the four arms of the side-2 plus at (3,2). Figure 4 shows the position before its last move.
Since the blocks are forced, every position of the forced tree below the second reply is determined by the line, and the first player's stones at any point are the opening pair and a prefix of it. Committing to the line makes the forced tree a function of the reply pair, which the argument for boards of size at least 17 uses.
The Python implementation of the rule was run over every reply pair on each board from 6 to 17. Every board plays exactly the 79 lines of the region, since a pair's line depends only on its abstraction. On the 6 × 6 board, 985 reply pairs need no tempo move, 91 need one, 54 need two, and 25 need three; the 79 pairs needing two or three tempo moves have both replies in the region and are the same on every board, while the other two counts grow with the board. Every pair won by a side-1 plus needs no tempo move and every pair won by a side-2 plus needs at least one. The longest line, the second game above, has six first-player moves after the opening pair, and every game in which the second player always blocks ends by ply 17; a reply that blocks nothing leaves a threat that the rule completes at its next move. So the rule wins every game by the seventeenth ply. This bound is computed from the 79 lines and is not part of the formal theorem.
The second player has no winning strategy on any board, by strategy stealing. Had the second player a winning strategy, the first player could open with an arbitrary move and thereafter follow that strategy as if the extra stone were absent, making a further arbitrary move whenever it selects an occupied cell. Surplus stones never hurt, so the first player would win, against the assumption that the strategy wins for the second player. For the first player has no winning strategy either. For the board has at most four cells, so neither player ever holds four. For an exhaustive search that is part of the formal development exhibits, for every first-player move, a reply after which the first player still cannot force a win. The step from neither player forcing a win to each player securing a draw is determinacy of the finite game, proved by induction on the number of empty cells. So the boards up to 4 × 4 are drawn under optimal play.
The 5 × 5 board is won by a table, extracted from a full solution of the 5 × 5 game ( positions solved, with draws scored against the first player) and verified by a checker that walks the complete game tree, every reply at every node. Like the rule, it completes a square when it can and otherwise blocks one before consulting the table. It opens at (2,2), gives a second move for each of the 24 first replies, and after the second reply follows a forcing plan where one exists. For 104 of the reply pairs, with the table's second move, the solver finds no winning continuation of at most eight moves in which every first-player move makes a threat, so the table plays a quiet move there, one making no threat, and continues with a sub-table indexed by the reply. Such a position is a branch point (Figure 5). That no such continuation exists is a computation of the solver and is not formalized; the win of the table is. The table plays in Figure 1 when n is set to 5.
Fix a strategy and a board size. The full tree of the strategy is the game tree in which the first player's moves are given by the strategy and the second player's moves range over all empty cells; the strategy verifies if every branch ends in a first-player square, and then the first player wins. The 5 × 5 table is checked on its full tree.
The rule is checked on a smaller tree. The forced tree has the first player playing the strategy's move, the second player's replies ranging over all empty cells at the first two levels, and below every later node only over the cells that block a threat of the move just played. The checker walks this tree under four guards. (G1) After the second reply, every move of the strategy wins outright or makes a threat. (G2) Every non-winning move and every threat cell lies in the region. (G3) After every move of the strategy the second player has no threat. (G4) Optionally, for a given cell, no move of the strategy has that cell as its only threat cell. A reply that blocks nothing leaves a threat standing, which the strategy completes at its next move, so every omitted reply loses in two plies. The soundness theorem of the forced checker says that if a strategy plays a completion whenever one exists and its forced tree passes the guards with every branch ending in a first-player square, then the tree in which the first player plays the strategy's move at every node is winning.
The rule passes the forced tree on every board from 6 to 17, one run of the checker per board, with reply pairs at the root, from 1,155 pairs at 6 to 82,368 at 17; the runs take from under a second to 72 seconds each. At every node the checker evaluates the rule afresh; no table is consulted. A Python implementation of the rule and a full-tree verifier, used while the rule was being found, agree with the Lean definition on the line committed to for every reply pair of the 6 × 6 board and for the anchored positions of the next section, and the full-tree verifier confirms the win on 6 × 6. Only the Lean runs enter the proof. The bot on this page is a TypeScript copy of the rule, and the site's tests replay it against the lines the Python implementation commits to on the same positions.
For every the first player following the rule wins. A stone beyond the base board can affect the rule's play only through a hidden corner, and the rule never lets a block land on one. The proof replays a checked run on the 23 × 23 board as a run on the larger board. Replies inside the base board are read verbatim. A reply beyond the base board is replaced, for the base run, by a stand-in: a fixed cell beyond the base board when the pair has no hidden corner, and an anchor, a cell beyond the base board that forms with the other reply the same hidden corner, when it has one. The anchor board, 23 × 23, is the least board holding every anchor. The anchor board, the stand-ins, and the anchors are choices made in the proof, and the rule does not depend on them.
The simulation theorem is stated for any strategy. Take a real history of the opening pair and two replies on a board of size at least 17, and a base history on another board of size at least 17 with the same first-player moves, in which each reply is either the same cell inside the base board or, for a reply beyond the base board, some cell beyond the 12 × 12 corner. Suppose that (i) on every history extending the real one in which the first player's stones lie in the region, the strategy plays a cell completing one of the first player's squares whenever one exists; (ii) the strategy plays the same move after the real history and after the base history, whatever further moves follow both; (iii) the forced tree of the strategy below the base history passes the guards, with a chosen cell as the cell of (G4) if there is one, and every branch ends in a first-player square; and (iv) if a reply lies beyond the base board, then either no cell was chosen and the reply pair has no hidden corner, or the chosen cell is the pair's hidden corner. Then the tree in which the first player plays the strategy's move at every node below the real history is winning. For the rule, hypotheses (i) and (ii) are lemmas about its definition. The rule's move depends on a history only through its abstraction and through the second move of the first reply; a reply beyond the base board and its stand-in both drop out of the abstraction, the stand-in pair is chosen with the same hidden corner as the real pair, and every first reply beyond the region, and every stand-in, has the default second move (3,2), so the two abstractions agree at every node.
Pairs with a hidden corner are covered by three families of anchored runs, each a forced run of the rule on the anchor board from the opening pair and an anchor pair, with as the cell of (G4), preceded by a check that is the hidden corner of the anchor pair. The far family, for both replies beyond the base board, uses the anchors and , two corners of the square of side 17 anchored at ; one run per cell of the region, 36 runs. The exact family, for a first reply inside the base board and a second reply beyond it, keeps the first reply, which lies in the row or the column of at distance at least 12, and places the second anchor at the corner opposite of the square through and the first reply; 70 runs. The far-near family, for a first reply beyond the base board and a second reply inside it, is the exact family with the two replies exchanged; 70 runs. This gives 176 anchored runs in all. The theorem for boards of size at least 17 dispatches five cases to the simulation theorem: neither reply beyond the base board, which is a branch of the forced run on the anchor board; a reply beyond it and no hidden corner, with the stand-ins (22,22) and (22,21), again a branch of that run; and the three cases with a hidden corner, one per anchored family.
The Lean development defines cells, boards, and squares as above, and the
winning predicate P1CanWin as an inductive family whose
derivations are exactly strategy trees: one first-player move per node,
every reply covered, draws failures by construction. The second player's win
is defined from it by swapping roles after a move; the first player's
ability to secure a draw is a second inductive family, whose branches may
also end on a full board, and the second player's is defined from that by
the same swap. Strategy stealing and determinacy are proved against these
definitions with no computation. These definitions, a few dozen lines, are
the whole specification; everything else is proved against them.
The predicate behind the theorem for the rule is WinsWith. For
a strategy σ, a board size n, and a history
h with the first player to move, WinsWith σ n h
holds if the move of σ at h is legal and either
completes a square or admits at least one reply, no reply completes a
second-player square, and WinsWith holds again after every
reply. It implies
P1CanWin by forgetting that the move is the one
σ returns. The theorem for the rule is
theorem plus_wins_with {n : ℕ} (h : 6 ≤ n) :
WinsWith plusMove n []
where plusMove is the rule as a Lean definition, 250 lines with
no data beyond the seven exceptional second moves. Three executable checkers
are proved sound: the table checker, the forced checker, which is generic
over strategies, and the refuter for the small boards. Each soundness proof
is an induction over the checker's recursion, so it never inspects the
strategy. Hypotheses (i) and (ii) of the simulation theorem for the rule are
plusMove_takesWins and plusMove_agree, proved by
unfolding the definition; the simulation theorem is simulate,
and the outcome theorem is outcome. Concrete boards are
discharged by native evaluation (native_decide): the
refutations at 1 to 4, the 5 × 5 run, one evaluation for the rule's runs at
sizes 6 to 16, one for 17, one for the anchor board, and one per anchored
family. The axioms of outcome and plus_wins_with
are therefore propext, Classical.choice,
Quot.sound, and one instance of Lean's evaluation axiom per
certificate; the kernel checks the soundness theorems but not the
evaluations, which the Lean compiler and runtime perform. The run on the
anchor board, 277,728 reply pairs, takes 499 seconds, the 176 anchored runs
take 0.34 seconds together, and the whole development builds in about 17
minutes. Both artifacts are built from this repository on every deploy:
the paper (PDF) and
the Lean development (tar.gz). The paper is on
arXiv as arXiv:2610.22410.
The rule wins by ply 17, a bound computed from its lines. What is the least ply by which the first player can force a win on the board, and is there a rule of comparable length that attains it on every board? The second move has seven exceptions; is there an opening, or an opening with a fixed second move, from which a rule of this kind wins with none? Whether a short rule exists for 5 × 5, where the table needs quiet moves at branch points, is open. Base 16 would serve the hidden-corner argument, but whether the rule still wins when it reads only the 16 × 16 board was not checked; whether a rule can read less than the second player's stones inside its base board, for instance only those inside the region with a summary of the rest, is open.