Claude's Fermat Proof Makes Verification the Product • The Weighted Average

Anthropic’s September 4 account of formalizing Fermat’s Last Theorem describes an 11-day effort consuming about six billion output tokens from an internal research model. At the public output price of the roughly comparable Claude Fable 5.1, that volume has an approximately $300,000 output-only price analogue—not Anthropic’s actual bill, but a useful warning that machine-checkable research needs a budget as well as a breakthrough.

Reconstructed on September 7, 2026, from records available by September 7; this holiday edition’s discovery window covers September 3–7.

The deliverable is a checked statement

The achievement is formalization, not a new proof that resolves an open conjecture. Anthropic says Claude converted the mathematics into a complete computer-checked Lean proof, producing about 13 million lines of code. Its account distinguishes 30,300 theorems proved along the way from 29,500 intermediate theorems used in the final proof. Preserving that distinction is a small example of the larger discipline: an impressive output count is not necessarily the count of artifacts needed to support the final result.

The public proof repository makes the work inspectable rather than leaving it as a narrated demonstration. Anthropic reports that Lean checked the proof using its three standard axioms and that a comparator confirmed the statement matched Mathlib’s statement of Fermat’s Last Theorem. The result is stronger than a model asserting that it has finished. There is a defined proposition and a checking process against which the assertion can be tested.

The economic calculation uses the research account’s approximately six billion output tokens and the $50 per million output tokens listed for Fable 5.1 in Anthropic’s September model announcement. Six billion divided by one million, multiplied by $50, equals approximately $300,000. The estimate inherits the rounding of the token count. It is a public-rate analogue for output volume, not a measurement of internal marginal compute cost or a price quote to reproduce the result.

Several exclusions are essential. The research model was only described as roughly comparable to Fable 5.1, not identical to the public model. The calculation excludes input tokens, caching, infrastructure, human guidance, and checking costs. It also does not apply a subscription allowance or assume that the same task would complete with the same token count on a different deployment. Those missing quantities prevent an honest all-in project budget, but they do not make the disclosed output volume economically meaningless.

The archive’s analysis of Fable 5.1’s cheaper cache reads explains why that exclusion matters. Discounts on rereading context do not automatically discount a large volume of generated output. Research operators should maintain separate measures for the work proposed, the tokens spent, and the artifacts ultimately accepted by a checker. Otherwise an attractive input tariff can obscure the cost of extensive exploration.

The coordination story is equally material. Anthropic says early attempts lost track of project state and stopped collaborating effectively. The successful effort used Prove2Me to maintain a dependency graph of theorem statements, separate statement and proof files to improve compilation, and support search and reuse. The lesson is not that adding more agents automatically creates a mathematical research group. It is that the shared work record and acceptance criteria became part of the system that made progress possible.

Buy a verification loop before buying autonomy

The near-term adopter is a research group working in a domain where results can be expressed in a formal language and checked against a stable specification. Such a group should start with a bounded target, an explicit statement, a pinned checking environment, and a reviewer responsible for the mathematical interpretation. The public success supplies a reason to test that workflow. It does not justify promising that a general-purpose agent will formalize any difficult result on demand.

The Lean comparator’s documentation describes the distinction between matching the intended statement, restricting permitted axioms, and acceptance by the kernel. It also makes clear that the checking environment and trusted inputs matter. Operators do not need to treat those as obscure implementation details. They define what the final acceptance claim means and which parts of the process remain outside it.

Formal verification cannot decide every question a reader cares about. A successfully checked statement may still be an unhelpful translation of the intended problem, rely on definitions a reviewer should examine, or come with an exposition too cumbersome for humans to learn from. Anthropic itself argues that a formal proof should accompany, rather than replace, a human-understandable account. A research publication needs both a dependable artifact and an explanation of why that artifact answers the question.

This is distinct from the earlier Claude result on Riemann-zeta bounds, where the central claim concerned new mathematics. Comparing output-token counts between those projects would not measure efficiency: the tasks, deliverables, and models differ. The useful continuity is the insistence on independent checks and reproducibility. Each project needs its own denominator before it can become evidence about the economics of research automation.

The strongest counterpoint is that a large public-rate analogue may exaggerate the practical cost of useful smaller projects. Anthropic reports a separate formalization experiment using consumer subscriptions, and internal compute need not cost the API list price. That is precisely why the $300,000 figure should remain an analogue rather than a sensational invoice. It establishes the scale of one disclosed output stream; it does not establish a minimum entry fee for mathematical research.

Today’s lead on OpenAI’s research-automation measurements asks whether agent activity becomes verified progress. Fermat supplies an unusually concrete answer for one project: a machine-checkable artifact with an explicit statement. The next economic question is whether comparable workflows reliably produce useful checked results across a portfolio of tasks, including failures, at an affordable total cost.

The verdict is to pilot the verification loop, not copy the headline agent count or elapsed time. Preserve intermediate statements, rejected attempts, model versions, usage records, and human interventions. Independent reproduction, a complete cost ledger, and repeated success on different formalization targets would strengthen the deployment case. A mismatch in the intended statement, fragile checking dependencies, or an inability to reproduce the result would weaken it. The proof is the product; autonomous activity is only one of its inputs.