atlas-lean

ATLAS 是一个由大型语言模型自动形式化的数学教科书库，涵盖了分析、代数、几何、拓扑、组合数学、概率论、统计学、偏微分方程、数论和理论计算机科学等领域的本科及研究生教材内容。该项目使用 Lean 4 语言将非正式的数学陈述和证明转化为可复用的形式化代码，旨在为未来的自动化与人工形式化工作提供基础构件。ATLAS 适合于需要高精度数学形式化验证的研究场景，如数学定理证明、算法正确性验证以及教育领域中对复杂数学概念的理解与教学。此外，项目还提供了一个可视化工具，便于用户浏览库中的内容，并比较非正式文本与其对应的 Lean 形式化版本。