First look at mathematics manuscripts from an internal frontier model at OpenAI

@edpegg Here’s a site where you can play the game you’re guaranteed to lose: snaky dot gotrevor dot org. You play White against a first-player win on 15 × 15, the board size in Harary’s conjecture.

The strategy comes from my own search, not OpenAI’s 21-move one, though their strategy closed the last three positions my search hadn’t. The write-up and a Lean proof of the 15 × 15 win are on GitHub at gotrevor/snaky-15x15. Claude Opus heavily drove this work.