Divide 13 million lines of Lean by 11 days and the run emitted about 1.18 million lines a day, close to 14 lines every second, without a pause [16]. Set the same file against the 100 pages of Wiles and Taylor's argument and each page of human prose expands to roughly 130,000 lines of code [17]. The 29,500 intermediate results average about 440 lines each [18]. None of those ratios measures mathematical difficulty. They measure how much a natural-language proof leaves implicit, and how cheap writing out the implicit part has become.
What the 11 days does not include is the substrate. The clock starts with an argument that was already finished and already repaired: Andrew Wiles worked on the problem for seven years in secret, announced in 1993, and then spent about a year with Richard Taylor fixing a flaw found in the proof [7]. It also starts with Mathlib, the central repository, already holding 2 million lines of formalised mathematics available to build on [5]. The agents were translating toward a target known to be true, with a specification in hand.
The run broke on coordination, not mathematics: several times the agents lost track of the project's state and stopped collaborating effectively, and progress came after Anthropic began using Prove2Me, a tool designed for human mathematical collaboration, to help agents track their work and pick next tasks [12]. Human experts also stepped in occasionally with high-level instructions to keep the work on track [11]. At this scale the binding constraint on a swarm of formalisers looks like coordination rather than proving.
Correctness is a different matter, and the mechanism is doing the work: a formalised proof sits in code that a machine grinds through step by step, which is what exposes a broken link [14]. Kevin Buzzard of Imperial College London drew the wider inference in his statement, saying the work shows autoformalisation of algebra, harmonic analysis, geometry and number theory, that such artefacts are now robust enough to be built upon, and that automatic formalisation of the modern mathematical literature is a big step nearer [10]. His is the only outside assessment in New Scientist's account, and it reached the public through Anthropic's own announcement [19].
So the demonstrated capability is narrower than the elapsed time suggests and still worth taking seriously: converting a settled, corrected human proof into machine-checkable form is now a days-long compute job, given a library beneath it and handlers watching. Buzzard's claim that these artefacts can be built upon is testable in the ordinary way, and the test is specific: the next formalisation project either imports the 13 million lines or re-derives them.
