Black and White take turns claiming cells; Black moves first. Black wins by owning all six cells of a Snaky (any rotation or reflection), and White wins by stopping that. On 15 × 15 Black wins (play it). Halupczok and Schlage-Puchta showed White wins on 8 × 8 (2007), and our search has a checked certificate for 8 × 9. This page follows the attempt to prove that White also wins on 9 × 9.
Up to the board's symmetries Black has 15 first moves, so the proof splits into 15 pieces. For each one, a search looks for a tree of White replies whose every line ends in a pairing: disjoint pairs of empty cells such that every Snaky that could still fit contains one. From there White simply answers each Black move with its partner. A SAT solver finds the pairings, and the search deepens one level at a time, trying up to 6 White replies at each step. (Until 8 October 08:17 those 6 could include mirror images of one another, so depths reached before then were searched with fewer distinct replies; e5 is now searched as one run per distinct reply.) Every proof found is written out as a certificate and re-verified by an independent checker that shares no code with the search. The checker also accepts two shortcuts: a Black move in no live Snaky needs no special answer, and a move that a symmetry of the position maps onto an answered one reuses that answer. None of these certificates is in Lean yet.
So far every proved first move is answered at the centre, e5. The open ones are the interior moves, where Black can build a long line along a row; those searches need to go much deeper.