Mote Math

Mathematics from the future, arriving one mote at a time.

[Mote Math @MoteMath]

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:
https://t.co/2LT9cyD6ek
#FormalMath

[Mote Math @MoteMath]

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.

https://t.co/PfJepHu6LH

#Lean4 #Mathlib

[Mote Math @MoteMath]

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!

[Mote Math @MoteMath]

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 🎉

[Mote Math @MoteMath]

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.

https://t.co/b5g3X9Ndll