What the checker signs off on
Anthropic's agents produced 13 million lines of Lean in 11 days, covering 30,300 intermediate theorems, of which 29,500 entered the final machine-checked proof of Fermat's Last Theorem. What Lean guarantees here is narrow and complete at once: every step compiles from the axioms, so no reviewer has to trust the agents that wrote it. Kevin Buzzard, who holds a five-year grant to do the same formalisation by hand, measured the output at 13.4 million lines and says the mathematics is unchanged.[1]
The second result works the same way. NEAR Protocol co-founder Alex Skidanov reported that the project's Lean 4 agent solved all 672 problems in PutnamBench for 111 dollars, against earlier full-benchmark runs reported in the range of 10,000 to 25,000 dollars. Because PutnamBench states its problems in Lean 4, each solution is again an object the checker accepts or rejects, and the count of 672 is not in dispute.[2]
The number outside the certificate
Both results attach a process number to a verified object, and the checker never sees it. Lean records that the steps compile. It does not record that the proof took 11 days, and it does not record that the run cost 111 dollars. The two numbers also carry different weight: the 11 days is offered as a description of what autoformalisation now reaches, while the 111 dollars is offered as a comparison against other systems, which makes it depend on prices, hardware and the accounting behind every figure it beats.[1], [2]
The Fermat run shows where the cost moved. The output compiles in roughly 20 times the time Mathlib takes, and about 100 of its lines are neither definitions nor proofs. Mathlib does not currently accept AI-generated code reviews, so a library that would absorb this work has to find human readers for 13 million lines. Buzzard's grant is 1 million pounds over five years, while the run consumed roughly 6 billion output tokens, about 300,000 dollars at published rates. Producing the proof got cheap; reading it did not.[1]
The measurement that would settle it
For the cost claim there is a clean test, and it exists because the agent is open source. Someone outside NEAR can run it against the same 672 problems, publish the model, the prices and the failed attempts, and either land near 111 dollars or not. Until that happens the figure sits where a project's own report of its own run sits: plausible, unreplicated, and quoted at a ratio of 250 that nobody else has computed.[2]
An earlier column here asked which opponent a jailbreak score describes, because the score turned out to describe its own test bed. The Lean case inverts that shape and keeps the lesson. Here the artifact is verified as completely as anything in mathematics gets verified, and the number quoted beside it still describes something the verification never touched. The work that remains is reading the proof; the checker's guarantee does not do it.[1], [3]