Thirteen million lines of Lean code. Twenty-nine thousand five hundred and eleven proved theorems. Eleven days.
That is what an internal Anthropic model produced when a researcher named Tianyi Peng set out, in early August, merely to test how far Claude could push the formalization of Fermat's Last Theorem. The result went further than he expected: the first complete, computer-checked, end-to-end proof of a conjecture Fermat scribbled in a margin around 1637.
Kevin Buzzard has held a five-year EPSRC grant to do the same job by hand. He compiled Anthropic's code himself, ran the standard checker over it, and blogged it up under the headline "Anthropic has beaten me to it."
And then, in the same breath, he said the result tells us nothing about mathematics.
That is the paradox worth sitting with. Buzzard puts the odds that Wiles's proof is correct at 99.9 percent, and says most of the number theory community sits at 100 percent. The formalization, he wrote, "just faithfully follows the early literature on the proof and adds nothing."
So the story is not "AI did math." The story is that AI just showed us which part of math was actually scarce — and it wasn't the part everyone was funding.
The story is not 'AI did math.' It is that AI showed us which part of math was actually scarce — and it wasn't the part everyone was funding.
Consider the arithmetic Buzzard himself could not resist. He was given £1m over five years. Anthropic took eleven days, and — his own aside — he wonders whether they spent more. The only public number is the run's six billion output tokens, roughly $300,000 at list price for the internal model, described as comparable to Claude Fable 5.1. Illustrative, not an invoice. But it sits against a million pounds and half a decade, and the comparison does not flatter the old model.
What was compressed here is verification, not discovery. Anthropic is explicit: unlike its earlier Riemann work, which produced novel mathematics, "what's novel here is the verification." Claude translated a known human proof — the Darmon–Diamond–Taylor exposition of Wiles — into a form Lean can check line by line, with no step waved through as "obvious," relying on only three standard axioms.
This is not a rounding error on Timothy Gowers's earlier point. In August, Gowers argued that the AI mathematics breakthroughs everyone quotes are counterexamples, not proofs. A complete machine-checked proof is a genuinely different object — and Fermat is the constructive mirror of his warning. Verification, it turns out, is the thing that industrializes.
Which is exactly why Terence Tao's warning, published the same week, is not the opposite story. It is the same one.
Tao took the Navier-Stokes regularity problem — a Millennium Prize question about whether smooth fluid flows stay smooth forever — and ran a thought experiment. The strategy for a blow-up solution is already roughly known: design a self-similar ansatz, find an approximate solution, prove stability under renormalization, verify the residual. Each step is fiendish for humans and highly coupled. Each step is also exactly the kind of pipeline AI plus interval arithmetic plus formal verification is built to run.
Now imagine an autonomous AI harness, flush with compute, running that entire loop internally — trying, failing, adjusting, and finally landing the correct ansatz. It produces a Lean proof so large no human can read it, and the company running the system keeps the whole path to the answer out of public view.
Technically, one of mathematics' most famous open problems is solved. And mathematics, Tao warns, gains almost nothing from it.
His reasoning is precise, and it is worth quoting the load-bearing line: "if we want this iteration to genuinely produce new understanding, the person or system doing the iteration had better not know in advance what the correct ansatz is." Knowing the answer suppresses the exploration of other routes — and it is those apparent dead ends, and why they fail, that historically carry the value.
Tao is not speaking abstractly. He never solved Navier-Stokes. But in trying, he accidentally linked fluid computation, Turing universality, and symplectic topology. The failure was the product.
He can point to the same field's genealogy: Leray–Hopf weak solutions, the Gagliardo–Nirenberg–Ladyzhenskaya inequalities, Prodi–Serrin partial regularity, the Beale–Kato–Majda blow-up criterion. None of these were the answer. All of them came from chasing it. Turbulence theory itself owes its philosophical shape to that chase.
So Tao's blunt conclusion: in the worst case, AI's effect on mathematics could flip from positive to net negative. A solved problem can be a loss to the field if the solving happens inside a closed harness that swallows every instructive failure.
Put the two stories together and the shared thesis surfaces. AI has decoupled verification from understanding. The checkmark at the end and the comprehension along the way are now two separate goods — and until this week the profession mostly paid as though they were one.
Fermat proves that decoupling is real and industrial. Tao shows what it costs if we keep pricing the two goods the same.
Here is the part the triumphant coverage skipped: the bottleneck did not vanish. It moved.
None of Claude's 13 million lines can enter Mathlib as things stand. Buzzard, a Mathlib maintainer, notes the library will not currently accept AI reviews. Reviewers are reluctant to read AI-generated code, because most of it is poor. The repository already carries around 3,000 open pull requests, more than 600 active in the review queue.
So the constraint has shifted from writing proofs to reading them — which is precisely the problem formalization was supposed to solve, reappearing one layer up. The scarce resource is now human review capacity and legible understanding.
Buzzard's own grant, tellingly, remains unfinished by Claude. It commits him not just to submitting foundational number theory to Mathlib, but to building a document that lets humans explore the modern proof. He doubts Anthropic will do the second. That second thing — the legible, teachable artifact — is exactly what the harness does not produce.
This is where the institutions come in, because norms, not models, are the live variable now.
Journals and funders should stop paying full price for "formalized." A machine-checked proof is a real and valuable object — it settles correctness beyond doubt — but it is not the same currency as "understood." Treating them as interchangeable rewards the checkmark and starves the exploration that produces the next generation of ideas.
The practical implication is concrete. Fund the byproducts: the failed ansätze, the lemmas spun off from dead ends, the human-readable exposition, the estimates a researcher develops en route. Tao offered a live example the same week — Julia Stadlmann's new estimates on smooth moduli reportedly got out and were credited, per [E2], just before an AI stampede on twin primes threatened to "pollute" the problem. Had she been slower, her method for equidistribution estimates on numbers with large smooth factors might simply have been buried under a wave of answers.
For Mathlib maintainers, the tension is sharper still. A library that will not accept AI reviews now faces submissions written faster than any human can vet — and the review queue, not the prover, is the wall.
The honest response is not to pretend the checkmark is worthless. It is to name what it is and is not. Anthropic's harness can now formalize thousands of pages of literature end to end; that capacity is real, and building on it will be tempting. The danger is mistaking a verified conclusion for an advanced field.
The week's two headlines look like triumph and warning. They are one instrument reading two dials. AI made proofs cheap to check and, if we are careless, understanding easy to skip — and the institutions that decide what counts as a contribution now have to price those two things apart.