facebookresearch/atlas-lean

来源：https://github.com/facebookresearch/atlas-lean

ATLAS - 大规模自动形式化教材库

ATLAS 是一个 Lean 4 教材数学库，由大语言模型自动形式化生成：将非正式陈述和证明翻译为 Lean 代码。它取材于本科和研究生阶段的教科书，涵盖分析、代数、几何、拓扑、组合数学、概率论、统计学、偏微分方程、数论和理论计算机科学。ATLAS 的目标是为未来人类和机器驱动的 Lean 形式化提供可重用的形式化构建块。

这项工作仍在积极推进中：我们继续扩展到更多来源，整理生成的材料，提升覆盖率和可维护性，并努力使该库更接近 Mathlib 的惯例。ATLAS 使用 AutoformBot（https://github.com/facebookresearch/autoform-bot）自动形式化管道生成。

链接

• 配套论文：大规模形式化数学（https://arxiv.org/abs/2605.29955）
• 形式化工具：
• 早期相关工作：代数组合学的形式化（https://github.com/faabian/algebraic-combinatorics）

库数据

Atlas/ 下每个图书目录包含：

• 生成的 Lean 源文件（定义、陈述和证明）。
• targets.yaml，列出选中用于形式化的教材陈述。
• report.json，包含匹配的 Lean 声明的自动评估结果，包括忠实度、证明完整性和代码质量得分。

可视化工具

可视化工具位于 https://rammalahmad.github.io/atlas/。用户可浏览 ATLAS，比较非正式陈述与其 Lean 形式化结果，查看结果之间的逻辑依赖关系图，并提取用于陈述选定定理所需的 Lean 代码。

ATLAS 可视化工具

状态与贡献

ATLAS 是一个持续进行的机器生成扩展项目，而非最终成品。我们正在积极扩展语料库、整理生成的代码、形式化剩余的陈述，并改进对 Mathlib 的习惯用法重用。欢迎外部贡献！

要使用固定的 Lean 和 Mathlib 版本构建完整库，请运行：

lake build

统计数据（2026年5月）

26 本书 · 630,999 行代码 · 483,917 行 Lean 代码（不含注释/空行） · 46,203 个声明 · 42,837 个已证明（92.7%） · 2,855 / 4,007 个陈述已形式化（71.3%） · 183,157M 个 token

贡献者

最初的 ATLAS 工作由 Ahmad Rammal、Niket Patel、Fabian Gloeckle、Amaury Hayat、Julia Kempe、Remi Munos、Charles Arnal 和 Vivien Cabannes 主导。

引用

如果您觉得这项工作有用，请引用我们的论文：

@misc{rammal2026formalizingmathematicsscale,
  title={Formalizing Mathematics at Scale},
  author={Ahmad Rammal and Niket Patel and Fabian Gloeckle and Amaury Hayat and Julia Kempe and Remi Munos and Charles Arnal and Vivien Cabannes},
  year={2026},
  eprint={2605.29955},
  archivePrefix={arXiv},
  primaryClass={cs.AI},
  url={https://arxiv.org/abs/2605.29955},
}