facebookresearch/atlas-lean

ATLAS是一个基于Lean 4的大规模自动形式化教科书数学库，由LLM生成。它涵盖分析、代数等多个领域，旨在提供可复用的形式化构建块，辅助人类与机器进行Lean代码的形式化验证与开发。