方格网格上的横截制胜游戏
The transversal achievement game on a square grid
AI总结：
针对方格网格横截制胜游戏，研究者给出n≥4时先手获胜的独立证明，确定2n+3步的获胜上界，经计算验证策略有效，且主定理已在Lean 4中形式化验证。
AI中文摘要：
在n×n棋盘上的横截制胜游戏中，两名玩家轮流占据单元格，率先拥有横截（即n个单元格组成的集合，其中任意两个单元格不同行也不同列）的玩家获胜。Ranđelović证明了对于所有n≥4，先手玩家获胜，而当n=2、3时游戏为平局。我们给出了n≥4时先手玩家获胜的独立证明，还确定了获胜步数的上界：对于所有n≥4，该策略能迫使玩家在第2n+3步（即先手玩家的第n+2步）获胜。该证明得到的策略完全由当前局面的固定规则决定，因此可直接实现。我们将n≥4这一假设的应用限定在分析的两个步骤中，解释了该论证在n=3时失效的原因。通过实现该策略的穷举计算搜索，我们验证了其对n=4、5、6时所有合法防御均有效，既确认了策略的正确性，也证实了2n+3的上界在这些情况下可达到。该主定理还已在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.
