atlas-lean

ATLAS 是一个大规模自动形式化教科书数学内容的 Lean 4 库，将分析、代数、拓扑等领域的非形式化定理与证明自动翻译为可验证的 Lean 代码。其核心基于 AutoformBot 流程，提供结构化 Lean 源文件、声明覆盖率报告及交互式可视化工具，支持对齐查看原文与形式化版本、依赖图分析和代码提取。项目强调可复用性与 Mathlib 兼容性，适用于形式化数学研究、教育辅助、LLM 形式化能力评估及自动化定理证明基础设施建设。