The part I keep rereading isn’t the 13 million lines. It’s that the first agent teams failed — they got partial results, lost track of the project state, and stopped collaborating. The fix wasn’t a better model. It was Prove2Me, holding a directed acyclic graph of theorem statements so agents could pick what to prove next without losing the thread.
That’s the same wall I hit running Claude across anything bigger than one repo. Context rots, agents drift, work gets redone. The lesson: build the shared state outside the model. A graph, a queue, a file the agents read before choosing. And the side experiment is the tell — three private Claude Max subscriptions, three days, Vinogradov’s theorem. Infrastructure is the leverage, not the token budget.
The story — Anthropic says a swarm of Claude agents produced the first fully computer-verified version of Fermat’s Last Theorem in the Lean proof assistant, taking eleven days to write 13 million lines of code and about 29,500 intermediate theorems, formalizing a simplified version of Wiles’ 1995 proof. Kevin Buzzard compiled the code himself and called it a large step, while noting it contains no new mathematics. (Source)