ATLAS (Autoformalized Textbook Library At Scale) addresses the challenge of formalizing vast amounts of mathematical knowledge by automatically translating informal textbook statements and proofs into Lean 4 code. It targets researchers and engineers in formal verification and theorem proving, providing a scalable foundation of reusable formal mathematical building blocks. The project aims to accelerate the development of formal mathematical libraries by leveraging LLMs for autoformalization.

How It Works

The core of ATLAS is the AutoformBot pipeline, which systematically converts informal mathematical content from undergraduate and graduate textbooks into formal Lean 4 definitions, statements, and proofs. This approach leverages LLMs to achieve unprecedented scale in formalization, generating a comprehensive library across diverse mathematical fields. Each book's formalization includes evaluation reports on faithfulness, proof integrity, and code quality, enabling systematic assessment and improvement of the generated artifacts.

Quick Start & Requirements

To build the full library, execute bash lake build. The project requires specific pinned Lean and Mathlib versions, managed via the lake build system. A visualizer is available at https://rammalahmad.github.io/atlas/ for browsing and inspecting formalizations. The autoformalization harness can be found at https://github.com/facebookresearch/autoform-bot. The companion paper is available at https://arxiv.org/abs/2605.29955.

Highlighted Details

• Formalizes content from 26 mathematics textbooks across various fields.
• Comprises over 630,000 lines of code, with 483,917 lines of Lean code.
• Features 46,203 declarations, with 92.7% of them proved.
• Achieved formalization for 71.3% of targeted textbook statements.

Maintenance & Community

ATLAS is an active, machine-generated extension effort led by Ahmad Rammal, Niket Patel, Fabian Gloeckle, Amaury Hayat, Julia Kempe, Remi Munos, Charles Arnal, and Vivien Cabannes. The project is continuously scaling its corpus, curating generated code, and improving alignment with Mathlib conventions. External contributions are welcomed.

Licensing & Compatibility

The license type and compatibility notes for commercial use or closed-source linking are not explicitly stated in the provided README.

Limitations & Caveats

As a machine-generated library, ATLAS is an ongoing effort requiring curation and refinement to fully align with Mathlib conventions. While proof rates are high (92.7%), the formalization of statements is at 71.3%, indicating ongoing work to cover all targeted textbook content. The project is not a finished product and is subject to the inherent limitations of automated formalization.