Fermat's Last Theorem in Lean, without the eight-hour build
Today we're putting out our first public release, and we're really happy it's this one.
The Lean formalization of Fermat's Last Theorem (anthropics/fermats-last-theorem) is one of the most ambitious things anyone has built on top of Mathlib: 60,475 modules of it. If you've tried to open it, though, you probably noticed it doesn't come cheap. The project pins Lean v4.33.1, but the Mathlib version it uses was built for v4.33.0, so Mathlib's usual download cache has nothing for it. You end up compiling all of Mathlib and then the whole formalization yourself. On our cloud machine, with 32 to 48 cores, that took about eight and a half hours.
So we compiled it once and published the results on Hugging Face, along with Mathlib and every other dependency at the exact versions the project expects. Clone the repo, run our small fetch script, and after a download of about 17 GB, lake build tells you all 69,184 jobs are already up to date. No compiling.
Get the builds, or start from the index, which has the fetch script and the list of everything we've released. The step-by-step instructions are on the build page. Before announcing, we ran them ourselves from a fresh account with empty caches, not signed in to Hugging Face.
What we checked
We didn't want to just hand over a pile of compiled files, so every build comes with its full build log and an axiom audit. For FLT, the audit traced all 1,134,828 declarations back to the axioms they rest on, and every one of them uses only Lean's three standard axioms. In Mathlib and a few of its dependencies, a handful of compiled definitions use lcProof, an axiom Lean's code generator adds to compiled code. We checked what kind of declaration each one is, and none of them is a theorem. We also had a second user with empty caches restore everything from scratch, to make sure nothing was missing.
A compiled build isn't a review of the mathematics, though. It tells you the code compiled; it can't tell you whether each statement says what its name promises. And Lean doesn't re-check .olean files when it loads them, so if you're relying on something, re-check it with lean4checker or build it from source.
These builds are unofficial. The formalization belongs to its authors, and we're not affiliated with them or endorsed by them. A big thank you to them and to the Mathlib community, whose work this all rests on.
What's next
This is the first piece of a longer research program. We think formal mathematics should be cheap to build on: compile something once, audit it, share it, and let people (and machines) get straight to the interesting part. We already have a lot more projects building and going through the same checks, and we'll release them as they pass.
If something on one of the build pages looks wrong, or you're an author who'd like a build changed or taken down, open a discussion in that repository's Community tab and we'll take care of it.