The square achievement game on $n \times n$ boards
Sean Reid
math.CO
Oct 14, 2026 · v1
TL;DR
All proofs, including the outcome theorem for every board size and the plus-rule strategy's soundness, are formalized in Lean 4 on Mathlib with verified checkers.
Abstract
Two players alternately claim cells of an $n \times n$ 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 $n \ge 5$, which answers a question of Erickson. For $n \ge 6$ 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 of size $6$ to $17$, and a simulation theorem carries one checked run on the $23 \times 23$ board to every larger board. The proofs are formalized in Lean 4, and the theorem for the rule states that the tree of its own moves is winning.
Problem
In the square achievement game, two players alternately claim cells of an n×n grid, and the first to hold the four corners of an axis-parallel square wins. Erickson asked for the outcome under optimal play. Before this work the cases 6 ≤ n ≤ 14 were open.
Approach
Strategy stealing and determinacy are proved directly against inductive game definitions. Small boards (n ≤ 5) are settled by exhaustive search and a verified strategy table. For n ≥ 6, a lookup-free 'plus rule' built from forcing moves is checked by a forced-tree checker proven sound in Lean, for boards 6 to 17. A simulation theorem carries one checked run on the 23×23 board to every larger board.
Results
The first player wins if and only if n ≥ 5, and boards with n ≤ 4 are draws. A single rule wins on every board with n ≥ 6, by ply 17. The Lean development has no sorry; it relies on standard axioms plus Lean's evaluation axiom for each certificate run.
| n | pairs | time (s) |
|---|
| 5 | full tree | 1.5 |
| 6 | 1,155 | 0.9 |
| 10 | 9,603 | 4.4 |
| 17 | 82,368 | 72 |
| 23 | 277,728 | 499 |
Reply pairs checked and checker run time per board size (selected)
