From a Classical Theorem to a Computer-Checked Proof
Fermat’s Last Theorem states that no positive integers a, b, and c satisfy aⁿ+bⁿ=cⁿ when the integer exponent n is greater than 2. Fermat wrote the claim in a seventeenth-century margin, but it was not proved until Andrew Wiles completed a modern number-theoretic proof in 1995. Anthropic now reports that Claude transformed this complex line of reasoning into an end-to-end formal proof in Lean in about 11 days, allowing a proof assistant to check it step by step.
What the Achievement Actually Changes
The central achievement is not a new discovery of Fermat’s theorem, nor a shorter replacement for Wiles’s proof. It is a change in verification. Human mathematical writing omits steps considered obvious and relies on a large body of prior literature; Lean requires those logical links to be made explicit in machine-readable form. According to the source, Claude generated about 13 million lines of Lean code and proved roughly 29,500 intermediate theorems used in the final result. The finished proof uses Lean’s three standard axioms.
The project also shows that the model alone does not explain the result. Dozens of Claude agents had to coordinate definitions, theorem dependencies, and progress. Early attempts stalled when agents lost the state of the project and collaboration broke down. The effort improved after the researchers used Prove2Me, a platform developed by Tianyi Peng and collaborators. It tracked theorem relationships in a directed acyclic graph, separated statements from proofs, and supported parallel work, search, and reuse. The source says the project consumed roughly six billion output tokens.
Practical Implications for Mathematical Research
Formal proofs could reduce part of the cost of reviewing difficult mathematical results. If a paper provides both a human-readable explanation and a compilable, independently checkable formal artifact, researchers can use machine verification as a separate quality-control layer, especially for AI-generated or AI-assisted arguments. Formalization may also expose gaps in existing mathematical literature and encourage more modern results to enter reusable infrastructures such as Lean and Mathlib.
The collaboration framework may matter as much as the model. The source also describes an experiment in which agents using three personal Claude Max plans formalized an application related to Vinogradov’s Three Primes Theorem in three days. This does not mean that any difficult theorem can now be solved reliably through consumer subscriptions. It suggests instead that task decomposition, dependency management, and reusable theorem libraries may determine outcomes more than a single prompt. For research groups, infrastructure and workflow will be central parts of AI-assisted mathematics.
Limits, Trust, and Open Questions
Passing a computer check is not the same as achieving complete human understanding. A formal system can verify a chain of reasoning in a specified language and axiomatic setting, but researchers must still establish that the theorem statement is correct, that the formal objects match the intended mathematics, and that the libraries and toolchain were configured appropriately. Anthropic says a comparator confirmed that the theorem statement matches Mathlib’s version of Fermat’s theorem. That is an important check, but it does not replace explanation of the proof’s structure and mathematical meaning.
Scale presents another practical challenge. At 13 million lines, the artifact is far larger than the principal library on which it builds, and some generated material came from failed attempts. Large formalization projects therefore need maintainable naming, dependency graphs, auditing practices, and long-term community support. The meaningful test in the future will not be only whether a model can make a root theorem display as proved. It will also be whether other mathematicians can reuse, inspect, modify, and understand the resulting work.
Moving Beyond a Single Milestone
If the report withstands further independent review and can be reproduced reliably in a public environment, it could become an important demonstration of automated formalization. AI would handle much of the mechanical translation, search, and coordination, while humans would choose mathematical strategies, define problems, and explain results. This division would not remove mathematicians from the process; it could shift more effort toward conceptual design and theoretical judgment. The formalization of Fermat’s theorem is therefore better understood as an infrastructure test than as the end of mathematical discovery.
The long-term value of this work will depend on transparency, reproducibility, and community participation, not simply on model speed. Mathematics may gradually expect important papers to include formal versions, but human-readable proofs will remain essential because they explain why a conclusion holds. The most durable future is likely one in which the two forms complement each other: machines provide fine-grained consistency checks, while humans provide structure, intuition, and meaning.