The final theorem depends on three standard Lean axioms
The repository states Fermat's Last Theorem for positive natural numbers and exponents of at least 3, then connects that statement to Mathlib's formulation. Its default target also checks that the final theorem depends on exactly three standard Lean axioms. Those are strong, inspectable claims in the source. They are still the project's claims rather than results from our sandbox, because we did not complete an independent build.
Anthropic describes this as a research artifact and says it is neither maintained nor open to contributions. That sentence should control your expectations. The useful object is a pinned proof tree at commit 6e837e7. A roadmap, support channel, and release cadence do not come with it. The source was assembled by AI agents, with Lean used as the arbiter, and the README warns that generated names may disagree with the mathematical meaning of their statements.
The browser exposes 29,511 theorem pages
Opening individual generated files is the hard way to understand this repository. The bundled html/ directory is about 390 MB and contains pages for 29,511 theorems and 1,450 definition modules. Each theorem page shows its Lean statement, what it cites, what cites it, and an expandable dependency graph. The static site works offline, so a clone doubles as a browsable archive without a web server.
The pages draw a clear boundary between source and explanation. The exact Lean statement is authoritative, while English summaries and suggested references were generated automatically. Browser testing covered Chromium-based software only. That makes the site a good index and a poor substitute for reading the formal statement when a detail matters. PROOF-PATH.md is the better starting point for the mathematical route because it names the theorem carrying each step.
What happened when we ran it
Our 3-CPU, 8 GB Debian sandbox did not run commit 6e837e7. The harness found no supported ecosystem for Lean, and the repository contains no Dockerfile that could supply one. It therefore produced no install duration, dependency count, build result, test count, or vulnerability scan. There is no failure log to interpret because no build command was started.
That result says something narrow but useful: this repository falls outside an ordinary automated project runner. It does not contradict the verification account in the README, and it does not confirm it. Anyone who needs independent assurance must reproduce the Lean build and the additional checkers on a prepared host. Our unprivileged container, which had no secrets, only established that the project does not provide a container path our lab could execute.
Rechecking needs Lean 4.33.1 and control of the host
The documented path starts with Elan, Lean 4.33.1, Mathlib v4.33.0, and network access. Mathlib is compiled from source because the pinned toolchain lacks a matching prebuilt package. The repository supports Linux and macOS, while warning that some paths are too long for Windows. Comparator and nanoda are separate verification routes with more tools to install, so lake build is only the first gate.
Issue 10 records a less obvious Linux requirement. Several fresh builds reportedly failed while reading compiled .olean files even though those files existed. A maintainer traced the behavior to the host's memory-map limit, and the reporter completed the build after increasing vm.max_map_count through sysctl. The issue remains open. That workaround needs host privileges, which rules out some managed runners and locked-down containers before CPU or memory capacity even enters the discussion.
The six-step map limits the scope of the named theorems
PROOF-PATH.md moves through reduction to prime exponents, the Frey package, irreducibility, modularity, level lowering, and the vanishing of a weight-2 cusp-form space. More useful than that outline is its statement of scope. The document says which forms of results associated with Mazur, Langlands-Tunnell, Wiles, and Ribet appear in the tree, then names broader versions it does not prove. That distinction helps a specialist avoid inferring a general theorem from a purpose-built lemma.
The attribution record identifies 106 files with material from the Imperial College London FLT project or flt-regular, plus 23 files that reproduce Mathlib text. The README also says comments were removed apart from limited notices, docstrings, and citations. So the proof may be machine-checkable while remaining awkward to learn from line by line. The dependency map and attribution table carry much of the explanation that ordinary library source would provide.
A September 24 push does not make this maintained
GitHub showed 1,237 stars and 6 open issues on September 29, 2026, and the latest push was September 24. The releases endpoint returned no published release. Those dates show recent publication work and reader attention, but the repository's own status is clearer: no maintenance and no contributions. Issue replies can still resolve a build problem, as happened in issue 10, without turning the artifact into a supported project.
Choose this repository when you want the completed claim, its exact formal statements, and a browser-visible dependency trail. Choose ImperialCollegeLondon/FLT when you want to work with an active formalization, flt-regular when the regular-prime case matches your research, or Mathlib when reusable Lean mathematics is the goal. For this repository, open the proof map before considering any local integration.