← All papers
First page of The transversal achievement game on a square grid

The transversal achievement game on a square grid

Kevin Guan

math.CO Aug 13, 2026 · v1
The main theorem that Player 1 wins the transversal achievement game for n≥4 is formalized and machine-checked in Lean 4.
In the transversal achievement game on the $n\times n$ board, two players alternately claim cells, and the first to own a transversal—a set of $n$ cells of which no two share a row or column—wins. Ranđelović showed that the first player wins for every $n\ge4$, while the game is a draw for $n=2,3$. We give an independent proof that the first player wins for $n\ge4$ that additionally establishes a bound on the length of the win: the given strategy forces a win by ply $2n+3$, i.e.\ on the first player's $(n+2)$-nd move, for every $n\ge4$. The proof yields a strategy that is fully determined by a fixed rule on the current position and can thus be implemented directly. We isolate the use of the hypothesis $n\ge4$ to two steps in the analysis, explaining why the argument fails at $n=3$. An exhaustive computational search implementing the strategy verifies it against every legal defense for $n=4,5,6$, confirming both the strategy's validity and that the $2n+3$ bound is attained in these cases. The main theorem has also been formalized and machine-checked in Lean 4.

In the transversal achievement game on an n×n board, two players alternately claim cells and the first to own a transversal (n cells with no two sharing a row or column) wins. The question is which player wins and how quickly.

An independent proof shows the first player wins for all n≥4, giving a strategy that forces a win by ply 2n+3 and is fully determined by a fixed rule maintaining an open-block invariant with matching theory. Two structural lemmas replace the case analysis of prior work. An exhaustive game-tree search implements the strategy against every legal defense for n=4,5,6. The main theorem is also formalized and machine-checked in Lean 4.

(c) A double threat.

The first player wins for n=1 and every n≥4, while n=2,3 are draws. The strategy forces a win by ply 2n+3, and exhaustive search confirms this bound is attained for n=4,5,6.

(a) Player 1 (X) win
nterminal linesnodes exploredmax win plyruntime
44 8756 075110.3 s
5485 760550 2241323.2 s
675 799 18582 103 245155 725 s
Summary of the exhaustive verification for n=4,5,6.