GoKawiilATLAS - Autoformalized Textbook Library At Scale
ATLAS is a Lean 4 library of textbook mathematics autoformalized by LLMs: informal statements and proofs translated into Lean code. It draws from undergraduate and graduate textbooks across analysis, algebra, geometry, topology, combinatorics, probability, statistics, PDEs, number theory, and theoretical computer science.
The goal of ATLAS is to provide reusable formal building blocks for future human- and machine-driven Lean formalization. This is an active effort: we are continuing to scale to more sources, curate the generated material, improve coverage and maintainability, and move the library closer to Mathlib conventions.
ATLAS was generated with AutoformBot, our autoformalization pipeline.
Links
Library Data
Each book directory under Atlas/ contains:
Lean source files for the generated definitions, statements, and proofs.
targets.yaml , listing the textbook statements selected for formalization.
, listing the textbook statements selected for formalization. report.json , containing automated evaluation results for matched Lean declarations, including faithfulness, proof-integrity, and code-quality scores.
... continue reading