Anthropic has published a repository containing a formal proof of Fermat's Last Theorem. Dozens of Claude agents translated a version of the classical argument by Wiles, Taylor and others into Lean, where a computer checks every logical step. The company says the effort took eleven days, generated about 13 million lines and used roughly 29,500 intermediate theorems in the final branch.

The word ‘proof’ needs care. Claude did not discover a new solution to the problem settled in the 1990s. The advance is an end-to-end machine-checkable translation of a large body of modern mathematics. It builds on years of work by the Lean and Mathlib communities and Kevin Buzzard's project; his positive expert assessment is important, but broader independent scrutiny of such a huge artifact is only beginning.

The agents succeeded after adopting Prove2Me, a platform that split the goal into a graph of smaller theorems, preserved project state and promoted reuse. The result therefore reflects orchestration, libraries and human-prepared foundations as well as model capability. The repository is public under Apache 2.0, allowing other teams to inspect and extend it.

If the method generalizes, it could convert papers into checkable form, expose hidden gaps and help review the rising volume of AI-assisted mathematics. Formal certificates might eventually accompany results used in cryptography, chip verification or safety-critical software. They would still not replace readable explanations or human judgement about whether the assumptions are appropriate.

Practical use requires reducing the extraordinary code and compute footprint, reproducing checks with independent tools and proving reliability on new work without such rich infrastructure. Optimistically, useful assistants for formalization teams could appear within 1–3 years and formal supplements for some papers within 3–7 years. Routine automatic checking of most new mathematics is further away and cannot yet be dated credibly.