The quiet math revolution (and where do we go from here)
OpenAI published 722 math manuscripts, many of them checked by the Lean proof assistant. What it says about brute force as intelligence, Terence Tao's Math 2.0, and what happens when math becomes a genie in a bottle.