Anthropic says Claude has completed a formalization of Fermat's Last Theorem in Lean. Its September 4 research announcement describes an eleven-day effort using an internal research model and collaborative agents. The company reports roughly 13 million lines of proof material and extensive automated work, with human direction and foundations supplied by the mathematical community.
The claim concerns a machine-checkable proof of an established theorem, not the discovery of a previously unknown result. It is also a claim about this research workflow, not a demonstrated capability of every publicly available Claude model. Anthropic describes the internal model as roughly comparable to Claude Fable 5.1. Newsroom has not rebuilt or independently verified the artifact.
A Hacker News submission on September 4 supplied a discovery signal, not technical corroboration. The release makes a useful distinction unusually concrete: generating an answer and supplying something that another system can check are different achievements. Understanding the result requires looking at the statement being proved, the assumptions allowed and the machinery doing the checking.
First establish what the proof actually says
Fermat's Last Theorem concerns the absence of positive integer solutions to a familiar power equation for integer exponents greater than two. Its historical importance provides context, but the famous name cannot by itself establish what a computer has verified.
The relevant object is the formal statement and its definitions. A file can contain a theorem with a reassuring name while encoding something weaker, different or unintentionally trivial. Readers evaluating an AI-generated formalization therefore need a route from the intended mathematical proposition to the exact statement accepted by the checker.
Anthropic's released repository includes a final checking entrypoint and a comparison procedure. Its documentation identifies the Lean and Mathlib versions and explains how to build the artifact. That makes the claim more inspectable than a screenshot of a successful session, although inspectability does not mean that Newsroom or an independent third party has performed the checks.
For an evaluator, the first practical question is simple: where is the statement that will be checked? The next is whether the relevant definitions can be followed without relying on the generator's description. Keep those questions visible even when the theorem itself is famous.
Then ask which assumptions are permitted
The repository's final check specifies three standard Lean axioms: proposition extensionality, classical choice and quotient soundness. It also describes checks intended to exclude unproved placeholders and unwanted assumptions. Those details matter because a proof's conclusion is conditional on its logical foundations.
This is not a demand that every reader inspect millions of lines manually. It is a demand that the verification claim identify its boundary. A proof accepted under an explicit foundation can be a precise technical result. An unspecified assurance that the system checked itself is much harder to assess.
The Lean comparator project addresses a related problem by checking a submission against a reference specification, constraining axioms and invoking kernel verification. In this context, comparison and proof checking serve complementary roles. One helps establish that the submitted statement matches the intended target. The other checks whether its proof follows within the accepted system.
A useful review note should record both results separately. If the proof checks but the target differs, the original claim remains unanswered. If the target matches but proof checking fails, the artifact has not supplied the required justification. The two questions should not collapse into a single success badge.
Separate another checker from another investigator
Anthropic also reports checking with the Rust-based nanoda kernel, using disclosed patches. That is a different checking implementation within the reported research process. It should not be described as an independent external replication unless another party has actually reproduced and documented the result.
The distinction applies beyond mathematics. Independence can refer to code, an organization, a dataset or an investigator. Saying which kind is present makes an account more useful. Here, implementation diversity may help examine reliance on one checker, while external reproduction would add a separate layer of evidence about the released materials and instructions.
The repository describes substantial computational requirements for a complete rebuild and comparison. A reader unable to run those steps can still inspect the version pins, commands, assumptions and disclosed modifications. That is a preliminary review, with a narrower conclusion than successful execution. Reporting that limit is part of an accurate account, not a reason to ignore the artifact.
A checked result does not explain every intermediate decision
Formal validity and mathematical readability answer different needs. A checker can accept an argument that remains cumbersome for a person to navigate. Researchers may still want shorter dependencies, clearer explanations or a better account of why a particular route was chosen.
This creates two useful evaluation tracks. One asks whether the artifact proves its stated target under the declared assumptions. The other asks whether it helps people understand, maintain or reuse the mathematics. Progress on the first should not be quietly presented as completion of the second.
Likewise, the size of the output is a description of the project, not a direct measure of insight. A large artifact may contain many intermediate results and operational choices. Evaluating its significance calls for examining what those pieces establish and how they relate to prior human work, rather than treating line count as a quality score.
What to look for in the next verification claim
For future AI results, ask for a named target, an executable artifact, explicit assumptions and a reproducible checking path. Then distinguish checks reported by the developer from checks performed by others. These questions form an assessment framework, not a claim that every domain can offer the same guarantees as formal mathematics.
Our earlier EEBench analysis illustrates that boundary. A simulated circuit result still leaves physical questions to test. A formal proof has a different verification target, with its own specification and software assumptions. Both become easier to assess when the report states exactly what passed and what remains outside the test.
Anthropic is the developer and publisher of this research, and its supplied lead artwork is illustrative. The released artifact gives technically equipped readers a concrete route to examine the company's claim. The next meaningful evidence is the outcome of that examination, with the checked target, toolchain and remaining trust assumptions stated plainly.
