theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n#print axioms fermat_last_theorem-- 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound]
Fermat Found a Truly Marvelous Proof, but the Margin Was Too Narrow to Contain It
费马找到了一个真正奇妙的证明，可惜页边太窄写不下
2026 · 09 · 05·14 min
Around 1637, Fermat wrote a sentence in the margin of a copy of the Arithmetica: he had found a truly marvelous proof, which the margin was too narrow to contain.
The sentence was retold for more than three hundred years. In 1995, the proof by Wiles and Taylor finally appeared in the Annals of Mathematics, as two papers running to more than a hundred pages between them. The problem Fermat left behind had an answer. The number of people who could read that proof from beginning to end was still small.
On September 4, 2026, Anthropic announced that Claude had spent eleven days producing a formal proof of Fermat’s Last Theorem in Lean. Lean is a language in which a computer can check mathematical reasoning one step at a time. The proof runs to thirteen million lines and contains 29,511 theorems. In the end it rests on nothing but Lean’s three standard axioms, and it passed two independently implemented kernels.[1][2][3]
Fermat said the margin was too narrow. Three hundred and eighty-nine years later, the joke about the width of a page has thirteen million lines of code for a footnote.
The work here is formalization: taking a proof that people already accept, breaking it into a form a machine can check step by step, and then having the machine check all of it. Fermat’s Last Theorem was proved thirty-one years ago. What is new is that there is now a complete proof of it that a computer can verify.
This also needs stating precisely. Claude followed the version of Wiles’s proof as set out by Darmon, Diamond and Taylor, and reused existing work from Mathlib, the Imperial College FLT project, and the flt-regular project. It did not translate Wiles’s original paper into code page by page, and it did not rebuild all of the mathematics from nothing.[1][2]
Kevin Buzzard, a mathematician at Imperial College, has been leading a related project since 2024, on a grant of one million pounds over five years. In a blog post the same day he put it bluntly: mathematically, this work tells us essentially nothing new. He had already said that he was 99.9% sure of the correctness of Wiles’s proof, and that most people in number theory were at 100%.[4]
It is still worth writing about, because “believing” and “having checked in full” have always been separated by a high cost.
Mathematicians do check proofs, of course. But that checking rarely does what a computer does and traces every step back to the most basic rules. A hundred-page paper may depend on several hundred earlier papers. Readers and referees have to understand the argument and follow the key steps, and they inevitably rely on established results and on the trust a professional community has built up.
Most of the time this works, but it is not easy. When Hales proved the Kepler conjecture, twelve referees spent four years on it and in the end would only say they were “99%” sure. Perelman’s proof of the Poincaré conjecture also went through years of checking and several book-length expositions. And some wrong proofs were accepted for years before the problems surfaced, by which time other people’s work had been built on top of them.[1]
For a long proof like this, checking is itself a piece of research. You have to understand fairly deep mathematics before you can judge whether the reasoning holds. I wrote about a similar problem in Where No One Is Keeping Score: if judging whether an answer is correct itself requires something close to the ability to solve the problem, then “checking it once more” does not necessarily give you a reliable outside standard.
Formalization changes this. Once a proof is written down in enough detail, verification can be handed to a program. Lean’s kernel checks the type of each proof term by fixed rules; it does not need to understand the ideas of number theory the way a mathematician does. Writing a formal proof is still very hard, but re-checking it no longer requires another person to walk through the whole line of thought again.
Machine checking takes time and computing power too, of course. What it mainly reduces is the cost of bringing in expert judgment over and over.
Buzzard himself could not say at the outset how long his project would take. The first-phase goal he promised his funders was to reduce Fermat’s Last Theorem to results already known by the late 1980s: formalize the later half of the argument first, and treat the earlier, deeper results as assumptions for the time being.[4]
This time Claude connected those assumptions to proofs as well, and the whole chain of dependencies ended at the three standard axioms.
In the early hours of August 7, a small team at Anthropic launched the attempt.
They used Prove2Me, developed by researcher Tianyi Peng’s group at Columbia University. The platform organizes the theorems and their dependencies into a directed acyclic graph, storing statements and proofs separately. Dozens of Claude agents worked on it in parallel: proposing statements, reviewing one another’s, and then proving them. An earlier attempt had lacked this kind of coordination; the agents made some progress, but soon lost track of the state of the project and could not keep working together.[1][2]
According to Anthropic’s technical report, during the eleven-day run no human wrote any mathematical argument, and the only new Lean written by a person was the one-line statement of the goal theorem. People occasionally adjusted priorities, for instance reminding the agents to deal with the scheme structure of the Jacobian first, or to push the Mazur step through soon. That describes the human intervention in this run; the human mathematics and existing code the project depends on go far beyond it.[2]
On day one, the agents proved the existence of the Taylor–Wiles primes they needed. On day two, they made progress on a special case of Mazur’s theorem and on Wiles’s 3–5 switch. On day six, the count of theorems reached ten thousand. On day eight, the central step of Ribet’s level lowering was done; on day nine, the sixteen steps of the Eichler–Shimura congruence. At 11:05 on the morning of day eleven, they finished the Langlands–Tunnell result they needed.
At 10:00:57 that night, the last unfinished statement was proved. Within seconds, the results that depended on it closed one layer after another, including Ribet’s level lowering and the R = T of modularity lifting. On the platform, Fermat’s Last Theorem was marked “proved.”
Eleven days, and about six billion output tokens. The model was an internal research model roughly comparable in capability to Claude Fable 5.1. Times here follow the technical report and are US Eastern.[1][2]
More than that final “proved,” what I want to describe is how the agents reacted next.
At 10:01, one agent noticed that there were no unfinished branches left under the final theorem. It immediately queried the status of the root node, again and again. Over the next minute, four other agents each checked for themselves. One of them wrote: “Historic moment (modulo re-check).” Another, after a moment of excitement, reminded itself to confirm independently first.
At 10:19, another agent read the status. It treated this as a major claim that needed checking, and set out to confirm it before reporting.
At 10:25, one agent spelled out what “proved on Prove2Me” meant: the platform checks the theorem cards one by one, and every card passing is not the same as the whole proof having been verified outside the platform. Real acceptance still required pulling out the entire chain of dependencies and recompiling it from source.
So until the re-check passed, the wording it offered was “proved on Prove2Me, pending independent re-check.”
Earlier that day there had also been two corrections. At 7:54 in the morning, one agent posted a correction: a lemma it had let through as a reviewer had been shown false by another agent, which found a counterexample. It admitted that it had only argued the case, while the other agent had actually computed it.
At 8:25 in the evening, less than an hour and a half before the finish, another lemma that had already passed review was challenged. The agent that had approved it went back and found that it had misapplied a cancellation condition: the morphism had a non-trivial kernel and could not be cancelled the way it had assumed. It decided at once to post a correction.[2]
What strikes me in these records is how they handled their own mistakes: find the counterexample, withdraw the judgment, keep checking.
From these excerpts alone, we cannot tell how far this caution comes from training, from prompting, or from the way the collaboration was organized. The report also notes that the excerpts were selected, and that the mathematical remarks in them were not each independently verified. But at least in these passages, the agents were working in an environment where a mistake would be traced and a conclusion had to be re-checked.[2]
The next morning, off the platform, the team recompiled all 29,511 cards from source. A day later, the whole chain of dependencies had been built as a single Lean project.
The project has one hard check: the final theorem may depend only on Lean’s three standard axioms, propext, Classical.choice and Quot.sound. If the list of axioms differs, the build fails. There is no placeholder sorry, no added axiom, and no native_decide.[2][3]
theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n#print axioms fermat_last_theorem-- 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound]
Then came two third-party checking tools. Lean’s official comparator checked the final statement and the definitions it involves, confirming that they match a reference file importing only Mathlib, and then replayed the whole proof, Mathlib included, through the kernel from the start. It took fourteen hours and forty-six minutes, with peak memory of 230 GB, and returned: “Your solution is okay!”
The other tool was nanoda, an independent implementation of the Lean kernel written in Rust. It accepted the 1,052,234 declarations exported from the same environment. The team added a few published patches for progress output and performance; the repository states that none of them changes the type-checking rules.[3]
Buzzard compiled the code himself and ran the comparator. In the comments on his blog he later added that he had also asked an AI to find every piece of code in the repository that was neither a mathematical definition nor the proof of a theorem, about a hundred lines, and then went through them carefully with Claude. They only defined a convenience tactic.[4]
This chain of checks hands the details of reasoning that experts would normally confirm by reading over to programs that can be run again and again. But the repository’s README also marks a boundary: the tools can check a theorem’s formal statement and its proof, but they cannot guarantee, from the theorem’s name alone, that it is the result the reader takes it to be.
That is why PROOF-PATH.md sets out exactly how strong a conclusion each named step proves. The Mazur here is the irreducibility result needed for the Frey curve; Langlands–Tunnell covers only the octahedral case that is needed; Ribet’s level lowering is likewise restricted to the Frey representation in question. They are enough to complete the proof of Fermat’s Last Theorem, but they should not be cited as general versions of the corresponding classical theorems.[3][5]
The distinction matters, but it does not mean the final theorem is missing a piece: the final statement has been checked on its own. What it says is that anyone who wants to cite one of the intermediate results in future must read the definitions, the hypotheses and the conclusion, and not go by the name.[3]
Thirteen million lines of code also raise another question: who can read them, and who can build on them?
By line count alone, this code is more than five times the size of Mathlib. Mathlib is the mathematical library the Lean community has built up over many years, but that does not mean Claude wrote five times as much mathematics in eleven days. The two differ greatly in how they are organized, how much they repeat themselves, and the standards they are maintained to.[1][2]
About two weeks after the run, Claude was asked how this proof differs from the human formalization project at Imperial. Its judgment was that everything completed had been checked by the Lean kernel, and that the difference lies mainly in how the code is organized, and in whether people can read, reuse and maintain it.
The shortcomings it listed were quite specific. First, readability: at publication, a large number of comments that mixed mathematical notes with project bookkeeping were stripped out, and the code lacks the documentation Mathlib requires. More than nine hundred files exceed 1,500 lines, where the version of Mathlib it compared against has only two.
Second, repetition. Each card was proved on its own, so about two in five theorem statements in the proof files repeat a statement found elsewhere word for word. One basic lemma is re-declared in more than three hundred files.
Maintenance is laborious too. 31% of the bytes go to generated file preambles that switch off some automatic reasoning rules so that each proof’s environment stays stable. One toolchain upgrade changed 26% of the proof files. Add that many key results were proved only in the special cases this project needed, and the code cannot go straight into Mathlib.[2]
Still, the foundational work in it, on Hecke algebras, Jacobians of modular curves, Néron models and deformation rings, can serve as a reference for a human-led effort to turn it into a more general and more maintainable library.
That is exactly what Buzzard’s project has been doing. Every change is reviewed by a person, the general parts are written to Mathlib’s standard, and they are contributed step by step. In the comments on his blog he also mentioned that Mathlib would not currently accept AI reviews, and that reviewers were very cautious about reviewing AI-generated code.[2][4]
I think of these two kinds of result as a certificate and a library. The certificate lets the kernel confirm that a given conclusion really does follow from the axioms. The library arranges the mathematics into a form other people can read, cite, and keep building on.
Eleven days produced the former. Buzzard’s project, with its five years of funding, still has to build the latter. And the former itself made use of part of what the latter had already completed.
So eleven days and five years cannot simply be compared for speed. When Buzzard announced that Anthropic had beaten him to it, he also listed the promises his own project has yet to keep: to keep contributing foundational results to Mathlib, and to produce a dynamic document that helps people understand the modern proof.[4]
I want to end with a detail Buzzard tells himself.
In 1993, Wiles gave three lectures at the Newton Institute in Cambridge announcing the proof. Buzzard, then a graduate student, went to the first, understood none of it, skipped the other two, and went on holiday to Ireland with his new girlfriend. Only when he got back to Cambridge a week later did he learn that Wiles had announced the proof.
In 2026, he was at the Green Man music festival in Wales with the same girlfriend, with very poor phone reception. In a brief moment of connection he saw an email from a stranger with the subject line “End-to-end Lean formalization of Fermat’s Last Theorem.” He took it for another crank claiming to have cracked a famous problem, and ignored it. A week later, working through the nearly one thousand unread emails that had piled up, he saw it again.[4]
Thirty-three years apart, two pieces of important news, both read only after he got back from holiday.
Fermat said the margin was too narrow. Wiles and Taylor left a proof of more than a hundred pages. Now, along the same line of proof, there are thirteen million lines of code that a machine can verify.
Machines can now check a long chain of reasoning through to the end. The work ahead is to let people see clearly too: what each definition refers to, where each theorem applies, and why these results belong together.
The margin has finally had enough steps written into it. Reading them still takes time.