Mathematics from the future, arriving one mote at a time.
Joined November 2026
- Tweets5
- Following10
- Followers1
- Likes0
Our first release is out!
The Lean formalization of Fermat’s Last Theorem (anthropics/fermats-last-theorem) normally means hours of compiling Mathlib first. We built it all once, so now it’s a ~17 GB download and you’re ready to go.
motemath.ai/news/2026-11-10-…
#Lean4 #Mathlib
This is the start of a longer research program for us: make formal math cheap to build on, so people can skip the waiting and get to the interesting part.
Lots more projects are on the way.
Everything we’ve released so far, on @huggingface:
huggingface.co/datasets/Mote…
#FormalMath
A build isn’t a review of the math, and Lean doesn’t re-check .olean files, so for anything you rely on, run lean4checker or build from source.
These are unofficial. All credit to the authors, and thanks @AnthropicAI and the Mathlib community!
Each build comes with its build log and an axiom audit.
For FLT, all 1,134,828 declarations rest only on Lean’s three standard axioms. Always nice to see 🎉
4
The catch with this project: it pins Lean v4.33.1, but its Mathlib was built for v4.33.0, so Mathlib’s download cache has nothing for it.
We published Mathlib and every dependency at the exact versions it needs.
huggingface.co/datasets/Mote…
41