Formalizing Mathematics at Scale

Published in arXiv, 2026

We introduce ATLAS (Autoformalized Textbook Library At Scale), a Lean 4 library of textbook mathematics autoformalized by LLMs. ATLAS draws from undergraduate and graduate textbooks across analysis, algebra, geometry, topology, combinatorics, probability, statistics, PDEs, number theory, and theoretical computer science. The library was generated with AutoformBot, our autoformalization pipeline.