Anthropic has open-sourced a complete, machine-checked proof of Fermat's Last Theorem in Lean 4 under the Apache 2.0 license, built on top of the Mathlib math library. The repository's formal statement reads: for any n ≥ 3 and positive integers a, b, c, a^n + b^n ≠ c^n. In Lean, that line becomes a theorem the kernel can verify step by step, with no gaps left open.
Scale is the most immediately visible part of the project. The repository counts 60,475 modules, 29,511 theorems, and 1,450 definition modules, with export checking covering 1,052,234 declarations. The generated HTML documentation runs about 390 MB, and the full export file is 37.8 GB. Reproducing the run locally requires more than 300 GB of disk space and peaks at roughly 153 GB of memory.
Three separate checks, each with a paper trail
The repository doesn't just assert that it compiles. The first check is Lean 4.33.1's own full kernel compilation, which took 5 hours 32 minutes on a 96-core machine. The second is a re-verification using leanprover's official comparator tool (v4.33.0), which ran for about 14 hours 46 minutes. The third swaps in an independent kernel written in Rust, nanoda 0.4.13, which finished in roughly 30 minutes on 16 threads and printed Your solution is okay!
Beyond the three checks there's one more hard constraint: none of the modules may contain axiom, sorry, native_decide, unsafe, extern, implemented_by, partial def, or #eval. In the Lean community, these keywords are well-known back doors — sorry literally marks something as unproven, and native_decide hands part of a judgment off to machine code the kernel never checks. Ruling all of them out amounts to admitting that the proof's credibility rests entirely on the Lean kernel and the checking tools — which is exactly what the README says.
How much of it AI wrote, the repo doesn't say
According to the README, the Lean source was “produced by AI agents on top of human-written open-source Lean code, with Lean acting as the referee.” The exact split isn't disclosed — which modules were written by humans and which were generated by a model and then kicked back by the kernel for another pass isn't broken out anywhere in the public materials.
The human foundation is spelled out more clearly. 106 dependency files come from existing academic projects, mainly the FLT formalization effort led by Imperial College's Kevin Buzzard and flt-regular, which handles the Kummer regular case; another 23 modules re-prove material already present in Mathlib.
Set against the history of formalized mathematics, the jump in scale stands out. The Four Color Theorem was formalized by Georges Gonthier in Coq in 2005, and the Flyspeck project for the Kepler conjecture wrapped up in 2014 — both measured in person-years. When Buzzard's team launched the FLT project, the outside expectation was likewise a multi-year timeline. Exactly how much this repository has pulled that timeline forward depends on the real human-AI division of labor, which happens to be the one number that still isn't public.
Sources: Anthropic's public repository README and verification records, CocoLoop, the Mathlib project, Imperial College's public FLT project materials; module count, theorem count, and the three verification runtimes are checked against the repository's own figures.