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.
| Version | Status | Location | License |
|---|---|---|---|
| v2 | In development | Repository root | Apache 2.0 |
| v1 | Archived and available | v1/ |
Original v1 license |
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:
scripts/check.shThe existing Atlas/ developments and archived v1/ release are not part of
this root build. They retain their own build configuration.
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.
The complete first release—including its Lean sources, evaluation reports,
build configuration, documentation, and companion paper—is available under
v1/.
cd v1
lake buildUseful links:
- ATLAS v1 documentation and statistics
- Interactive visualizer
- Companion paper: Formalizing Mathematics at Scale
- AutoformBot
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.