Two players claim hexes, racing to link their opposite sides of a rhombic board. Hex can never end in a draw — when the board fills, exactly one player has a connecting path (a topological certainty). And a beautiful strategy-stealing argument proves the first player has a winning strategy: if the second player had one, the first could steal it — an extra move never hurts in Hex. We know a winning strategy exists without knowing what it is.
THE TECHNIQUE no draw + strategy-stealing ⇒ first wins
The demo checks a top-to-bottom connection and states the no-draw / first-player-wins facts: live demo
HISTORY & CREDIT Hein 1942 · Nash 1948
“Someone found the first player’s winning strategy for Hex.” — it is proved to exist (strategy-stealing) but is unknown for boards larger than 10×10. cited
no draw · a full board always has exactly one connected side (a topological fact). strategy-stealing · if player 2 could win, player 1 steals the strategy — contradiction; so player 1 wins. 1942/48 · Piet Hein and John Nash invented it independently.
A winner proven to exist, and still unknown. theorem
RECOMMEND FOR I-13 connectivity, on the compiler
On i-13, a column of stones forms a top-to-bottom chain; no-draw and first-player-win are the theorems:
$ i13 run gm_hex.i13
RUN OK · 35 step(s)
connects = 1 -- vertical chain top to bottom
no_draw = 1 first_wins = 1 determined = 1
Recommend as a NULL — existence theorem (B39) + connectivity (B39). The no-draw property and first-player win are pinned facts; the connectivity check is a fixed predicate. Existence without a construction is not a same-function DOF. NULL — someone must connect, so first wins.