Three layers of understanding
01 · Understand the problem
There are no positive whole numbers a, b and c with aⁿ + bⁿ = cⁿ for n bigger than two. Humans proved this in the 1990s. Claude's new achievement is turning the proof into instructions a computer can check.
02 · Understand the contribution
Anthropic reports that Claude produced an end-to-end Lean formalization in 11 days, with approximately 29,500 intermediate theorems. Mathematician Kevin Buzzard publicly commented on the resulting artifact.
03 · Academic context
This is an autoformalization result, not a newly discovered proof of an open conjecture. In Lean, each proof term is checked against axioms and library definitions by a small kernel. Trust still depends on the assumptions, formal statement and checker; it is not evidence that the model's private reasoning has been revealed.
What this might change
Demonstrates a possible path to auditing long mathematical arguments at scale, reducing verification labor while shifting attention to specifications and dependencies.
What is NOT established
The theorem was already proved by Andrew Wiles. Formal verification does not establish that every explanatory step in natural language is correct.