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

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 placements in total. The finite proof object uses a conservative abstraction which truncates adjacent coordinate gaps to five, separately on the two axes. We prove preservation of winning lines, coverage of every legal second-player placement, and implementability of relative first-player actions in every concrete preimage. Thus 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. We describe the mathematical soundness argument, the recorded verification, and the requirements for a portable release. The bound is an upper bound, not an assertion of optimality. Preprint, version 1. Not externally peer reviewed. This record contains the manuscript only. The complete certificate corpus and portable verification package are not publicly available; full reproduction from the deposited files is not yet possible. The paper distinguishes the completed local certificate verification from future artifact release and clean-environment replication. 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.