Chomp the poisoned chocolate bar
A bar of chocolate whose bottom-left square is poisoned. On your turn pick any square and eat it together with every square above and to the right of it. Whoever has to eat the poison loses. The first player always has a winning bite — a strategy-stealing argument proves it — but the argument does not say which one. The computer here knows: it has solved every position of the bar. With hints on, the winning bites are lit up.
bars with more than one winning bite
recomputed and checked
How the computer knows
Every position reachable from an m×n bar is a staircase: row k (counted from the poisoned bottom row) keeps rk squares, with r0 ≥ r1 ≥ … . There are C(m+n, m) of them, and the combinatorial number system numbers them 0, 1, 2, … without gaps. A bite lowers the first row it touches and leaves the rows below it alone, so in lexicographic order of rows every position comes after everything it can move to. One sweep in that order labels each position lost (no move reaches a lost position) or won.
Three rows, and one number off on a well-known page
With three rows there is a shortcut. For each q ≥ r exactly one p makes (p, q, r) lost, and Andries Brouwer's recurrence finds it as a minimum excluded value along a row and a column. Run to q = 16,000, it reproduces his tables, Gabriel Nivasch's lists of rows whose pattern repeats with period 2, 3, 4 and 9, and four OEIS sequences — except one entry: Brouwer's list of rows where p − q settles to a constant has 95 where the computation (and the box solver, and his own list of positions (p, p, r)) says 94.