tl;dr: Scott Aaronson describes a hypothetical "Mathocalypse" in which OpenAI dumps 372 solutions to major open math and CS theory problems — including the Unique Games Conjecture, L=BPL, sub-O(n log n) integer multiplication, and partial progress on Riemann and Hodge — generated by an internal model using ~3 hours of compute per problem (~5% success rate on 8,000 attempts). The proofs come with Lean certificates but are nearly unreadable, triggering a scramble among mathematicians to decipher them. Aaronson contrasts OpenAI's "raw dump" approach with Anthropic's model of letting human researchers digest and announce results, and reflects on what mathematical research looks like now.