Fermat's Last Theorem was proved by Andrew Wiles in the 1990s, but a different mathematical milestone has now been reached: the proof has been translated into a form that a computer proof assistant can check line by line. An AI-assisted project reportedly produced about 13 million lines of Lean code in 11 days, turning one of modern mathematics' most celebrated arguments into a formally verified object.
This is not a new proof of Fermat's Last Theorem. The underlying mathematics remains Wiles's work and the later refinements that completed the argument. Formalization means expressing every definition, assumption and intermediate step in a precise logical language so that software can verify that no inference depends on an unstated gap.
That task is far harder than copying equations into a computer. Human mathematical writing relies on shared background knowledge and routinely compresses steps that experts consider obvious. A proof assistant accepts none of that. Libraries must contain the relevant algebra, number theory and geometry, and the formal proof must connect each step using rules the system recognizes.
The reported scale — roughly 13 million lines — illustrates the difference between a readable human proof and its machine-checkable counterpart. AI can accelerate the labor by proposing formal statements, filling routine gaps and searching libraries for applicable lemmas. Humans still have to define the goals, maintain the formal environment and evaluate whether the automated steps correspond to the intended mathematics.
Formal proofs have a different value from conventional peer review. They do not decide whether a theorem is important or whether a definition captures the right scientific idea. They do provide extremely strong assurance that, given the encoded assumptions and definitions, the logical steps are valid. For very long arguments, that can expose hidden dependencies and make later reuse easier.
The Fermat project is also a test of AI as mathematical infrastructure rather than as a chatbot that produces an answer. If models can reliably translate advanced literature into formal systems, large areas of existing mathematics could become searchable, composable libraries of verified results. New proofs could then build on those libraries with much less risk that an overlooked technical lemma contains a gap.
The speed of the reported formalization is what makes the result striking. Work that once demanded years of specialist effort may increasingly be divided between mathematicians and automated agents. That does not make human proof obsolete. Fermat's Last Theorem remains Wiles's theorem; the new achievement is giving a proof assistant enough explicit mathematical structure to verify the enormous chain of reasoning for itself.