ATLAS - Autoformalized Textbook Library At Scale
Summary
ATLAS is a Lean 4 library for autoformalizing textbook mathematics into Lean code, generated by an AI pipeline. It aggregates material from multiple textbooks, provides a visualizer, and tracks automated evaluation metrics for formalized content. The project is ongoing, with goals to scale, improve coverage, and align with Mathlib conventions, while inviting external contributions.