On 5 September 2026, Anthropic announced that its Claude model had produced the first fully computer-checked proof of Fermat’s Last Theorem. Eleven days. Thirteen million lines of Lean, more than 30,000 supporting theorems, roughly five times the size of Mathlib. Kevin Buzzard of Imperial College London, who started a human-led project to do exactly this job in 2024 and whose funding runs to 2029, reviewed it and said it proves the theorem “with no assumptions other than the axioms of mathematics”.
The line that travelled fastest was Decrypt’s summary: a proof “a computer can check itself, no human trust required”.
That is true. It is also precisely half of the thing, and this series exists for the other half. Welcome to the fiftieth.
TL;DR
- Anthropic says Claude formalised Fermat’s Last Theorem in 11 days, producing a 13-million-line Lean proof a machine can check line by line, with mathematician Kevin Buzzard confirming it holds.
- Machine-checking removes a real and enormous cost: Wiles’s 129-page proof had a hole found after he announced it, and it took a year to close.
- What it does not remove is the statement. A checker verifies a derivation relative to a sentence somebody wrote, and no machine tells you the sentence was the right one.
- Crypto’s version: a Chainlink VRF proof says “this output is the unique VRF output for this key and this seed”, and nothing else. It does not say the seed was beyond the operator, or that the number was mapped to a winner honestly.
- Satoshie’s fairness claims are five sentences you can check against deployed bytecode. Short enough to read is a design property, and one you can lose by growing.
What actually got removed
Formalising a proof means rewriting it in a language so literal that a proof assistant can verify every step without judgement, taste or charity. Anyone bothers because checking, not proving, has always been the bottleneck. Wiles announced Fermat across three lectures in June 1993, a reviewer found a hole, and he spent nearly a year closing it with Richard Taylor before publishing the corrected 129 pages in May 1995. One proof, from one of the best in the world, and it still took a year of expert attention to establish it was true. A machine checker deletes that cost: small, deterministic, no reputation to protect, never tired at page ninety. Spectacular result, and I will not hedge it to set up a punchline.
The fiftieth unasked half: the statement nobody read
Here is the part the headline cannot carry. A proof is never just a proof. It is always a proof of a statement. The checker verifies the derivation. It does not, and structurally cannot, verify that the statement at the top of the file says what you think it says.
So what exactly was Buzzard reviewing? Not the thirteen million lines. Nobody read those, that is the entire point of them. He was checking the top of the file: the definitions, and the sentence claiming to be Fermat’s Last Theorem, confirming that a formal expression in Lean encodes the thing Fermat scribbled into a margin in 1637. That is a human act, it needed one of the few people on earth qualified to perform it, and it is not automatable even in principle, because “does this formal sentence mean the informal thing” is a question about meaning, and meaning sits outside the system doing the checking.
Trust did not disappear, then. It moved, from 129 pages almost nobody could check to one sentence almost anybody can. A magnificent trade, and a trade rather than an abolition. For this series’ running ledger: verification is closed, meaning is not. A checker returns true relative to a statement, and nothing inside the machine will ever tell you whether that statement was the one you cared about.
Crypto has been shipping this exact half for years
Every “provably fair” badge in this industry is a proof of a statement, and near enough nobody reads the statement. Take the one we use. A Chainlink VRF proof is verified by the coordinator contract, on-chain, before the callback fires. No human in the loop, no discretion, no appeal. Same shape as Lean: a checker, a proof, and no request for your faith. Now read the sentence it proves. It says: this output is the unique VRF output for this public key and this seed. That is the whole claim.
Note what is not in it. It does not say the seed was outside the operator’s control, or that the number was mapped to a winner honestly, or that the entrant list at the moment of mapping was the real one, or that the prize was funded, or that the ticket count was contract state rather than a figure on a dashboard. None of which is a criticism of VRF, which is superb at the exact sentence it proves and has never claimed a syllable more. The failure sits with platforms that quote the proof and skip the sentence, and players who accept a logo as an argument.
The twenty-fifth instalment argued that a proof is a permission to check rather than the act of checking, because nobody runs the verifier. The twenty-sixth argued that verifying a component says nothing about the seams between components. This is the third and most uncomfortable: even when the check is run, and is mechanical, and passes, the statement it passed against was written by a person with interests.
Our statement, written out, so you can read it
If everyone should publish the sentence, we go first. Satoshie’s fairness claims, as things you can check against deployed bytecode rather than adjectives on a landing page:
- The ticket price is a constant in the deployed contract, not a setting behind an admin panel.
- The odds are a function of entry count, published before a single ticket is sold.
- The VRF proof is verified on-chain before the payout callback runs, not after, and not by us.
- On coinflip, the escrow, the callback and the payout occur in one transaction, so there is no window in which a human sees the result and then decides anything.
- No admin key reaches a live draw.
That list is the statement. The contract is the proof. If the list is wrong, verifying the contract perfectly earns you a flawless proof of the wrong thing, which is worse than no proof at all, because it arrives with confidence attached.
Notice the property that makes the list usable: it is short. Five sentences, readable over a coffee. Small enough to read is a design property, and one you lose by accident, feature by feature, until your fairness claim is a forty-page document nobody finishes. Thirteen million lines are checkable and unreadable at once, and this industry keeps collapsing those two axes into one.
The honest limits
We have not formally verified our contracts. Nobody in crypto gaming has, at any scale worth the word. The twenty-sixth instalment said outright that formal verification is priced out of this sector. That excuse started expiring this week: eleven days of machine time on the most famous theorem in the popular imagination means the cost curve for a few hundred lines of Solidity is heading somewhere new, fast. Judge us on it in a year, and if it still has not happened, the honest reason will be priorities rather than price.
Verification would only prove the code matches the specification, and we write the specification. Verified code with a wrong spec is a perfect implementation of a mistake: the statement problem again, one level down. Formal methods do not escape it, they relocate it, exactly as Lean did.
Checkable is not the same as clean. Roughly 7% of the lines in the Fermat proof are residue from early false starts, agents duplicating work before the coordination tooling landed. It all checks. Some of it does nothing.
Three questions to take with you
Ask what sentence the proof proves, and make them write it down. If a platform cannot produce the statement in plain language, there is not one, and the badge is decoration.
Ask where the sentence ends. A VRF proof begins at the request and stops when the callback fires. Everything either side of that boundary is somebody’s word, and the interesting money is usually parked just outside it.
Ask whether you could read the statement in a minute. If the answer is a PDF, the proof may be immaculate and you have still verified nothing. You have delegated, which is the thing you came here to stop doing.
Fifty
The Fermat result is the most complete verification our species has ever produced, and the final human step in it was one mathematician reading one sentence and nodding. That step does not vanish with a bigger model or a longer proof. It gets smaller, and correspondingly more load-bearing. Which is the whole ambition here: not a world with no trust in it, because nobody has built one, but a world where the trust left over is a five-line statement you can read yourself, in public, before you put money on it. Anyone selling “no human trust required” instead has not read their own statement either.
