How AI agents and human supervision produced a 126k-line Lean proof of the low individual-degree test, and what we learned about statement drift, review gates, and long-horizon proof composition.

Watching the Millennium Prize Problems fall one by one to AI, from a seat fairly near the front — on test-time scaling, formal proof, and what AlphaGo taught us about our own field.