The Curiously Playable Universe

AI achievements in mathematics may owe less to machines gaining access to mathematical intuition than to decades of human work turning mathematics into structured, playable environments, with creativity shifting from solving problems toward designing representations. AlphaProof solved three of the five non-geometry problems at the 2024 International Mathematical Olympiad by working in Lean, where proofs are mechanically checked. The same pattern appears in programming, where higher-level abstractions shift effort toward representations, and in physics, where Lagrangian and Hamiltonian formulations reorganize Newtonian calculations.