facebookresearch/atlas-lean

ATLAS is a large library of university-level mathematics that has been automatically converted from textbook form into a formal, machine-verifiable format called Lean 4. Lean is a programming language designed for writing mathematical proofs in a way a computer can check for correctness, rather than relying on human review. The conversion process, called autoformalization, was carried out by AI language models that read informal textbook statements and proofs and rewrote them in Lean code. The library draws from 26 textbooks covering a wide range of advanced mathematics: real analysis, algebra, algebraic geometry, topology, number theory, probability, statistics, combinatorics, differential geometry, and theoretical computer science. As of May 2026, it contains about 631,000 lines of code, 46,203 mathematical declarations, and 42,837 proved results, which is a 92.7 percent proof rate. Roughly 71 percent of the target statements from the source textbooks have been formalized so far. The purpose of the library is to provide reusable building blocks for future mathematical formalization work, both for researchers doing it by hand and for AI systems doing it automatically. Having a large corpus of verified formal mathematics in one place makes it easier to train better AI formalizers, to test whether new tools can prove known results, and to build on existing proofs rather than starting from scratch. Each book in the library comes with the Lean source files, a list of which textbook statements were selected for formalization, and a report with automated quality scores covering faithfulness and proof correctness. A web-based visualizer lets you browse the library, compare the original informal statement with its Lean version, and see how theorems depend on each other. This is an active and ongoing project from Facebook Research. External contributions are welcome. The project is not a finished product but rather a growing corpus that the team is continuing to expand and curate.