A Computer-Assisted Proof of a First-Player Win in Infinite Freestyle Gomoku

Abstract

We present a computer-assisted proof that the first player wins freestyle Gomoku on the infinite integer lattice. Players alternately occupy an empty lattice point, and a consecutive run of at least five stones in any of four directions wins immediately; neither player has forbidden moves. The certified strategy starts at the origin and wins before the second player within 35 actual placements by both players combined. The finite proof object uses a conservative abstraction which truncates adjacent coordinate gaps to five, separately on the two axes, while retaining all stones. We prove preservation of winning lines, coverage of every legal second-player placement, and implementability of relative first-player actions in every concrete preimage. Distant play is represented rather than treated as a harmless pass. Symmetry reduces the first reply to 20 orbits covering 120 normalized positions. Bounded threat rules compress parts of the strategy while retaining counterthreats and actual move counts. A checker independent of the search reconstructs successor sets and checks the complete dependency closure. The bound is an upper bound, not an assertion of optimality. Preprint, version 2. This record supplies the revised English manuscript (25 pages) and its LaTeX source. The revision clarifies short-rule hypotheses and placement bounds, documents the complete rule-use census, includes a worked two-remote-component example, and supplies a frozen-source audit index and named rejection regressions. The complete certificate, all 1,482,906 selected dependencies, frozen verification sources, manifests and verification instructions are publicly available in the complete review release. The revised manuscript and audit supplement and versioned source snapshot identify the present revision. The original certificate and eight mathematical checkers are unchanged. Research-tool disclosure: OpenAI Codex with language-model assistance was used for research exploration, programming, debugging, and manuscript preparation. The author provided the research objective, strategic guidance, and project supervision. RV2 and Rapfi were untrusted move advisers only. Mathematical certificate acceptance was independent of their evaluations and of the search heuristics. No AI tool is listed as an author.