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
| Version | Status | Location | License |
|---|---|---|---|
| v2 | In development | Repository root | Apache 2.0 |
| v1 | Archived and available | v1/ |
Original v1 license |
Formalized mathematics libraries
The root Lake package is limited to five libraries:
| Directory | Purpose |
|---|---|
MathlibExt/ |
Reusable, fully proved extensions to Mathlib |
MathlibExtTest/ |
Tests, benchmarks, and diagnostics for MathlibExt |
CSLibExt/ |
Reusable, fully proved computer-science developments built on MathlibExt |
CSLibExtTest/ |
Tests and diagnostics for CSLibExt |
WantedExt/ |
Established results whose Lean implementation or proof is deferred |
Repository checks live in scripts/. Run the complete
root validation with:
The existing Atlas/ developments and archived v1/ release are not part of
this root build. They retain their own build configuration.
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/.
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.