ATLAS

Autoformalized Textbook Library At Scale
A large-scale Lean 4 library of textbook mathematics formalized with LLMs.

[!NOTE] ATLAS v2 is coming. The original release is preserved in v1/, while the repository root is being prepared for the next generation of the project.

Versions

About ATLAS

ATLAS translates mathematical statements and proofs from undergraduate and graduate textbooks into Lean. Its goal is to provide reusable formal building blocks for human- and machine-assisted theorem proving across analysis, algebra, geometry, topology, probability, statistics, and theoretical computer science.

The project was generated with AutoformBot, an autoformalization pipeline for developing Lean libraries at scale.

Explore v1

The complete first release—including its Lean sources, evaluation reports, build configuration, documentation, and companion paper—is available under v1/.

cd v1
lake build

Useful links:

• ATLAS v1 documentation and statistics
• Interactive visualizer
• Companion paper: Formalizing Mathematics at Scale
• AutoformBot

Licensing

New work outside v1/ is licensed under the Apache License 2.0. Files inside v1/ remain subject to the original v1 license and are not relicensed by the root license.