Anthropic says Claude helped formalize Fermat’s Last Theorem in Lean

Anthropic has published new research describing how Claude was used to help formalize Fermat’s Last Theorem in Lean, a proof assistant that checks mathematical arguments line by line. The announcement is less about a model independently discovering a new proof and more about a practical frontier for AI in mathematics: turning highly compressed human proofs into machine-checkable formal code.

Fermat’s Last Theorem is one of the most famous results in mathematics. Andrew Wiles proved it in the 1990s, but the original proof depends on deep machinery from number theory and algebraic geometry. Formalizing a result of that scale is a different task from writing an explanatory proof in prose. Every definition, theorem dependency, transformation and logical step has to be made explicit enough for a proof assistant to verify. That makes the work slow and exacting even for specialists.

Anthropic’s post presents Claude as a collaborator in this proof-engineering process. The model can propose Lean code, help translate mathematical statements into formal syntax, repair errors and suggest ways to connect intermediate lemmas. Researchers still have to decide whether a route is mathematically sound, review generated code and guide the system when the proof state becomes complex. In other words, the work shows meaningful progress in AI assistance, not an escape from human mathematical judgment.

The result matters because formal proof is one of the harder tests for language models. A model can sound persuasive while being wrong, but Lean does not accept a proof unless the logic type-checks. That creates a feedback loop where many mistakes are caught automatically. It also changes what success looks like. Instead of asking whether an AI can write an elegant proof paragraph, researchers can ask whether it can steadily help complete verified artifacts inside a strict formal system.

For the broader AI market, the research points toward a future where models help with scientific and technical knowledge work by handling tedious translation, search and repair loops. Formal mathematics, program verification and safety-critical engineering all require more than fluent text. They need auditable chains of reasoning and artifacts that external tools can check. If models become better at working inside those constraints, they could make expert teams faster without replacing the expert review that gives the result credibility.

Anthropic is also careful to frame the work as a step rather than a final destination. Large theorem formalization remains difficult, and the system still depends on human planning and correction. But the publication adds to a growing pattern: frontier AI systems are being evaluated not only on chat answers, but on their ability to produce verifiable work products in demanding environments.