ATLAS - Autoformalized Textbook Library At Scale

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

ATLAS is a Lean 4 mathematical textbook library automatically formalized by large language models (LLMs), which converts informal mathematical statements and proofs into Lean code. It covers various fields from undergraduate and graduate-level textbooks, including analysis, algebra, geometry, topology, combinatorics, probability, statistics, partial differential equations, number theory, and theoretical computer science. Its goal is to provide reusable formalized building blocks to support future human and machine-driven Lean formalization efforts.

原始信息汇总

数据集概述：ATLAS (Autoformalized Textbook Library At Scale)

ATLAS 是一个大规模的 Lean 4 形式化数学库，由大语言模型自动将教科书中的非形式化数学命题和证明翻译为 Lean 代码。其素材来源覆盖分析、代数、几何、拓扑、组合学、概率、统计、偏微分方程、数论和理论计算机科学等领域的本科及研究生教材。

该库的目标是为未来人类和机器驱动的 Lean 形式化工作提供可复用的形式化构建模块。该项目仍在持续扩展中，包括增加更多数据源、整理生成内容、提升覆盖率和可维护性，并逐步使其更接近 Mathlib 的惯例。ATLAS 是通过 AutoformBot 自动形式化流水线生成的。

数据集组成

在 Atlas/ 目录下，每本教材的子目录包含：

• Lean 源代码文件：包含生成的命题、定义和证明。
• targets.yaml 文件：列出选择进行形式化的教材命题。
• report.json 文件：包含对匹配的 Lean 声明的自动化评估结果，评估指标包括忠实度、证明完整性和代码质量得分。

数据可视化工具

提供一个可视化浏览器，网址为 https://rammalahmad.github.io/atlas/，用户可在此浏览 ATLAS 库、对比非形式化命题与 Lean 形式化代码、查看结果之间的逻辑依赖关系图，以及提取选定定理所需的 Lean 代码。

数据规模（截至 2026 年 5 月）

• 教材数量：26 本
• 总代码行数：630,999 行
• Lean 代码行数（不含注释和空行）：483,917 行
• 声明总数：46,203 个
• 已证明声明数：42,837 个（证明成功率 92.7%）
• 目标命题数：4,007 个
• 已形式化命题数：2,855 个（形式化覆盖率 71.3%）
• 总 Token 数：183,157M

各教材详情统计

教材名称	目标命题	已形式化	形式化覆盖率	总代码行数	Lean 代码行数	声明数	已证明	证明成功率	Token 数 (M)
AlgebraNotes	176	151	85.8%	5,037	4,409	274	261	95.3%	1,962.99
AlgebraicCombinatorics	39	37	94.9%	10,695	9,343	737	734	99.6%	1,440.73
AlgebraicGeometryI	186	112	60.2%	40,678	27,393	4,499	4,210	93.6%	7,629.26
AlgebraicTopologyI	171	110	64.3%	29,154	20,142	2,416	2,063	85.4%	10,323.27
AnAlgorithmistsToolkit	158	131	82.9%	9,656	8,234	712	668	93.8%	2,004.00
ArithmeticGeometry	335	266	79.4%	39,257	29,573	3,047	2,861	93.9%	11,100.62
BooleanFunctions	108	44	40.7%	9,516	7,949	667	614	92.1%	2,327.49
Buildings	74	44	59.5%	64,383	48,809	4,345	4,247	97.7%	20,442.93
CombinatorialOptimization	36	22	61.1%	8,908	7,934	428	414	96.7%	2,475.65
ComplexVariables	38	37	97.4%	7,231	6,225	285	280	98.2%	1,250.91
DifferentialAnalysis	113	88	77.9%	31,302	23,713	1,634	1,506	92.2%	11,743.27
DifferentialGeometry	147	112	76.2%	10,592	8,942	888	781	88.0%	1,933.97
EllipticCurves	360	212	58.9%	32,819	22,316	3,483	2,981	85.6%	11,058.00
FourierAnalysis	38	34	89.5%	7,943	6,671	373	359	96.2%	1,185.90
GeometryOfManifolds	72	40	55.6%	22,686	16,408	3,251	3,098	95.3%	6,864.93
HighDimensionalStatistics	73	65	89.0%	39,656	31,715	1,564	1,518	97.1%	975.36
IntroductionToFunctionalAnalysis	72	68	94.4%	2,709	2,006	113	109	96.5%	553.64
IntroductionToPartialDifferentialEquations	105	86	81.9%	27,666	20,740	1,585	1,414	89.2%	2,972.23
LieGroups	185	74	40.0%	60,285	50,594	4,219	3,814	90.4%	45,384.33
NumberTheoryI	576	460	79.9%	64,958	54,760	3,764	3,591	95.4%	15,424.36
ProbabilisticMethodsInCombinatorics	210	109	51.9%	20,555	15,604	1,272	1,089	85.6%	2,720.15
ProjectionTheory	111	73	65.8%	13,357	9,672	979	871	89.0%	2,678.00
RealAnalysis	177	175	98.9%	2,886	2,224	149	147	98.7%	585.64
TensorCategories	229	137	59.8%	42,812	29,729	3,373	3,176	94.2%	11,338.45
TheoryOfComputation	118	84	71.2%	15,094	10,581	1,553	1,482	95.4%	3,580.36
TheoryOfProbability	100	84	84.0%	11,164	8,231	593	549	92.6%	3,200.61
总计	4,007	2,855	71.3%	630,999	483,917	46,203	42,837	92.7%	183,157

构建方法

使用锁定版本的 Lean 和 Mathlib 构建整个库，执行以下命令：

bash lake build

贡献者

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

搜集汇总

数据集介绍

构建方式

ATLAS是基于大规模语言模型自动形式化构建的Lean 4数学库。其构建流程依托于AutoformBot管道，从涵盖分析、代数、几何、拓扑、组合数学、概率统计、数论及理论计算机科学等领域的26本本科与研究生教材中，选取待形式化的陈述与证明，借助大语言模型将其自动翻译为可验证的Lean代码。每个教材子目录均包含生成的Lean源文件、标注了形式化目标的targets.yaml以及存储自动化评估结果的report.json。

使用方法

ATLAS的使用方法简洁明了：用户可通过运行`lake build`命令，配合固定的Lean与Mathlib版本构建完整库，从而在本地环境中利用已形式化的数学内容。此外，项目还提供了在线可视化界面（https://rammalahmad.github.io/atlas/），方便研究人员交互式地探索库中结构、审阅自动化评估报告，并直接获取所需的Lean代码片段，为人工或机器驱动的后续形式化工作提供坚实基础。

背景与挑战

背景概述

ATLAS（Autoformalized Textbook Library At Scale）是由Meta AI研究团队主导，于2026年构建的一个大规模自动形式化数学库。该数据集聚焦于利用大语言模型将本科至研究生级别的教科书数学内容（涵盖分析、代数、几何、拓扑、组合学、概率、统计、偏微分方程、数论及理论计算机科学）自动翻译为Lean 4代码，旨在为人工及机器驱动的数学形式化提供可复用的基础构建模块。ATLAS的创建不仅推动了数学证明自动化的边界，也为数学教育与研究提供了结构化、可机器验证的知识资源。其核心研究问题在于探索大语言模型在复杂数学推理与形式化验证中的能力边界，并评估自动形式化代码的忠实度、完整性和质量。该数据集累计覆盖26本教材，包含超过48万行Lean代码与4.6万个声明，其中92.7%的命题已获证明，对形式化数学社区产生了深远影响。

当前挑战

ATLAS面临的核心挑战涵盖领域问题和构建过程两方面。在领域层面，自动形式化需克服自然语言数学陈述与形式化代码之间的语义鸿沟，尤其是非形式化证明中隐含的直观推理、未明确定义的对象及依赖上下文的符号约定，难以被LLM忠实捕捉并转换为严格的形式化论证。同时，确保生成代码符合Mathlib社区约定、保持可维护性和可扩展性也是一大难题。在构建过程中，挑战包括：如何从散乱的教科书源文本中精准提取待形式化的目标陈述；如何评估自动生成的证明与代码在数学上的正确性，而不仅仅是语法上的通过；以及如何高效过滤LLM产生的幻觉与错误。此外，在覆盖26本超过18万兆token的庞大体量下，维持一致的代码质量、减少形式化遗漏，并持续迭代以纳入新源，均构成了工程与算法上的巨大挑战。

常用场景

经典使用场景

ATLAS数据集作为大规模自动形式化的教科书数学库，其经典使用场景在于为数学定理的机器验证提供可复用的形式化构建模块。研究人员可利用该库中的Lean代码，将高等数学教材中的非形式化命题与证明转化为结构化的形式化语言，从而构建起从代数几何到概率论等众多分支的严谨逻辑体系。这一过程不仅加速了个别定理的机械化验证，更为机器学习驱动的数学推理奠定了数据基础，使自动定理证明系统能够基于高质量的形式化语料进行训练与评估。

解决学术问题

该数据集直面数学形式化领域长期面临的核心瓶颈——手工编写Lean代码耗时且覆盖面有限，难以满足大规模验证需求。ATLAS通过大规模自动形式化，将26本研究生级教材中的4007个数学命题转化为形式化声明，其中71.3%已成功形式化，92.7%的声明得到完整证明，显著提升了形式化数学的可扩展性与覆盖率。它有效支撑了数学定理的可靠性验证、形式化证明的自动化生成，并为机器学习模型在数学推理任务中的性能评估提供了基准，推动了人工智能与形式化验证的交叉融合。

实际应用

在实际应用中，ATLAS为自动定理证明系统、数学教育工具及交互式证明助手提供了丰富的高质量训练数据。自动化形式化系统可基于该库中的对齐例对进行微调，提升从自然语言到形式化代码的翻译准确率。同时，该库支持的在线可视化工具允许用户浏览形式化代码、比较非形式化陈述与Lean代码的对应关系，并提取定理的形式化声明，为数学家与计算机科学家协同编写形式化证明提供了便捷途径，加速了数学知识的形式化沉淀与复用。

数据集最近研究

最新研究方向

ATLAS数据集代表了人工智能辅助数学形式化领域的前沿突破，通过大规模语言模型自动将26本研究生与本科生教科书中的数学定理与证明转化为Lean 4形式化代码，覆盖分析、代数、几何、拓扑、组合学、概率统计、偏微分方程、数论及理论计算机科学等核心分支。该工作呼应了近年来形式化验证与机器学习深度融合的热潮，特别是自DeepMind和OpenAI在定理证明领域取得进展后，自动形式化成为加速数学严谨性验证的关键路径。ATLAS以超过48万行Lean代码、92.7%的证明成功率和71.3%的陈述形式化率，展示了LLM在复杂数学推理中的巨大潜力，为构建可复用、可扩展的数学形式化知识库奠定了坚实基础，并推动了人机协作验证范式从理论走向工程化实践。