The Curiously Playable Universe
Contraptions
AlphaProof, from Google DeepMind, solved 3 of the 5 non-geometry problems at the 2024 International Mathematical Olympiad using Lean, where proofs are mechanically checked. The result was 3 solved out of 5 non-geometry problems. The article argues this points less to AI gaining human-like intuition and more to mathematics, programming, and physics being turned into formal, verifiable “game board” representations that make automated proving feasible.
Why it matters
A domain becomes “playable” when its complexity can be compressed into a stable repertoire of actions and interactions with repeatable outcomes and feedback. The piece argues that play is a matter of degree and that far more of reality than expected can be turned into a game—so systems can then be built to beat it.
