Fermat's Last Theorem in Lean, without the eight-hour build
We've published compiled builds of the Lean formalization of Fermat's Last Theorem and the Mathlib it depends on. Download them and the whole project is ready to use, no compiling.
Mathematics from the future, arriving one mote at a time.