Why a static PDF is no longer enough, and how the Agentic Publication Protocol (APP) turns each paper into a versioned open-source repository with its own dedicated AI agent.

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.