Why in news?
Anthropic announced on 4 September 2026 that its Claude system had produced a complete computer-checked proof of Fermat’s Last Theorem. The announcement is the development behind the theorem’s renewed coverage in this edition. Andrew Wiles had already established the result, with the published proof appearing in 1995. What is new is formalisation: expressing the reasoning in a language that a proof-checking program can examine step by step. Anthropic says the work used Lean and took eleven days of largely autonomous activity. This is a company-reported achievement supported by a public research repository, not a new discovery of the theorem itself. It matters because long mathematical arguments are difficult to check exhaustively by hand. Machine checking can add a rigorous verification route, provided the formal statement and its assumptions match the intended mathematics.
The simple question behind a difficult theorem
The theorem concerns the equation an + bn = cn. When the exponent is two, positive whole-number solutions exist: 3² + 4² = 5², because 9 + 16 = 25. Fermat’s claim is that no such solution exists when the exponent is an integer greater than two.
The restriction to positive integers is essential. It excludes zero, negative values and fractions from the stated problem. Allowing zero would immediately create examples such as 0n + 1n = 1n. That would not contradict Fermat’s theorem; it would change the conditions of the question being asked.
Testing many possible numbers cannot prove the claim for every positive integer. There are infinitely many combinations and exponents to consider. A proof must establish a reason that covers them all, rather than report that a large search found no exception. This distinction separates mathematical proof from an impressive numerical experiment.
What Wiles’s work had already achieved
Fermat stated the problem in the seventeenth century, but a general proof remained elusive for centuries. Wiles completed the decisive work in 1994, with an important contribution from Richard Taylor. The papers appeared in 1995. Keeping completion and publication dates separate avoids making two descriptions of the same breakthrough seem contradictory.
The route to the proof connected Fermat’s equation with elliptic curves and modular forms. Elliptic curves are mathematical objects described by particular cubic equations, not ordinary ellipses. Modular forms are highly structured functions. Earlier work linked a hypothetical exception to Fermat’s claim with an elliptic curve having incompatible mathematical properties.
Wiles established the needed modularity result for a class called semistable elliptic curves. Combined with the earlier connection, this ruled out the hypothetical exception. The Abel Prize’s citation describes that chain of ideas. The achievement was therefore not an endless search through numbers but a structural argument linking different areas of mathematics.
What Lean checks
A written proof often leaves routine steps unstated because a trained reader can supply them. Formalisation makes the definitions and logical dependencies precise enough for software. Lean is a programming language and proof assistant used for this purpose. A proof assistant is a system for constructing and checking formal mathematical arguments.
Lean’s documentation distinguishes the tools that help construct a proof from the small trusted component that checks it. That component is called the kernel. Automated methods can propose or assemble reasoning, but the resulting proof object must satisfy the checking rules. Fluent explanatory text is not, by itself, an accepted proof.
This creates a useful separation between generation and verification. A system may make unsuccessful attempts while searching for an argument; those attempts are not validated merely because they were generated confidently. What matters is the final formal statement, the assumptions it uses and the checked reasoning that connects those assumptions to the conclusion.
What the public release claims
Anthropic describes the release as the first complete computer-checked proof and reports approximately thirteen million lines of Lean code. Those scale and priority claims belong to the company’s account. The work builds on human mathematics and existing open-source projects, rather than starting without definitions, libraries or earlier formalisation efforts.
The repository states Fermat’s result using positive natural numbers and exponents of at least three. It describes checks intended to exclude unfinished proof placeholders and additional assumptions beyond Lean’s standard foundations. It also reports verification using a second kernel implementation. These records make the checking approach inspectable, rather than asking readers to rely only on a promotional headline.
There is still a distinction between checking a formal proposition and deciding whether it expresses the intended real question. A correctly verified statement with altered definitions could prove something different. The repository addresses statement matching explicitly. Lean’s own guidance likewise treats the trusted foundations and precise formulation as part of assessing a proof.
Conclusion
The September development concerns a new verification artefact for established mathematics, not the first solution of Fermat’s problem. Its significance lies in making a large chain of reasoning available for mechanical checking and further inspection. The lasting contribution will depend on the reliability and reusability of that formal work, not simply the speed or volume of generated code.