ai4math-lean

ai4math-lean 是一个包含21个Lean 4形式化数学数据集的集合，所有问题都经过lean-server v4.21.0的机器验证。数据集总量为3,394,310个数学问题，其中1,273,472个包含证明，352,065个在v4.21.0版本下验证有效。数据集包含多个子集，如deepseek_prover、goedel_pset、nemotron_proofs等，每个子集都有不同数量的问题和验证状态。每个数据条目包含丰富的信息，如唯一标识符(id)、形式化陈述(formal_statement)、完整的Lean 4代码(lean4_code)、是否包含证明(has_proof)、证明内容(proof_body)、自然语言描述(natural_language)等。特别地，数据集还包含详细的验证信息，如验证状态(v4210_is_valid)、编译状态(v4210_compiles)、是否包含占位证明(v4210_has_sorry)和验证延迟(v4210_latency_s)。该数据集适用于文本生成任务，特别适合形式化数学、定理证明和数学验证相关的研究与应用。数据集采用Apache 2.0许可证发布。

ai4math-lean is a collection of 21 Lean 4 formalized mathematics datasets, where all problems have been machine-verified by lean-server v4.21.0. The dataset contains a total of 3,394,310 mathematical problems, among which 1,273,472 have associated proofs, and 352,065 are valid under the v4.21.0 version. The dataset includes multiple subsets such as deepseek_prover, goedel_pset, nemotron_proofs, etc., each with varying numbers of problems and validation statuses. Each data entry contains rich information, including unique identifier (id), formal_statement, complete Lean 4 code (lean4_code), has_proof flag, proof_body, natural_language description, and more. Specifically, the dataset also includes detailed validation information, such as validation status (v4210_is_valid), compilation status (v4210_compiles), whether it contains placeholder proofs (v4210_has_sorry), and validation latency (v4210_latency_s). This dataset is applicable to text generation tasks, and is particularly well-suited for research and applications related to formalized mathematics, theorem proving, and mathematical verification. The dataset is released under the Apache 2.0 license.

原始信息汇总

ai4math-lean 数据集概述

数据集基本信息

• 数据集名称: ai4math-lean
• 许可证: Apache 2.0
• 主要任务类别: 文本生成
• 主要语言: 英语
• 标签: lean4, theorem-proving, formal-mathematics, verification, math
• 规模类别: 1M<n<10M

数据集构成与规模

• 总问题数量: 3,394,310
• 包含证明的问题数量: 1,273,472
• 在 Lean v4.21.0 上验证有效的问题数量: 352,065
• 包含的子数据集数量: 21 个

子数据集详情

数据集名称	问题数量	包含证明的数量	在 v4.21.0 上有效的数量
compfiles	297	259	67
deepseek_prover	27,503	27,503	27,126
deepseek_proverbench	325	0	0
formal_conjectures	618	13	13
formalmath	5,560	5,556	2
goedel_minif2f	244	0	0
goedel_mobench	360	0	0
goedel_pset	1,732,594	263,589	9,755
goedel_test	8	0	0
hf_lean_workbook	29,750	29,750	29,208
hf_minif2f_lean4	231	0	0
hf_minif2f_v2	488	0	0
hf_tonic_minif2f	488	0	0
lean_proofs	98	97	15
lean_workbook_full	140,214	0	0
matholympiadbench	360	0	0
nemotron_proofs	1,349,950	915,078	285,867
numinamath_lean	104,155	31,615	0
proofnet	371	0	0
putnam2025	24	12	12
putnam_bench	672	0	0

数据模式与特征

每个数据行包含以下字段：

字段名	类型	描述
id	字符串	唯一问题标识符
source	字符串	数据集源名称
formal_statement	字符串	Lean 4 定理陈述（无证明体）
header	字符串	导入/设置代码
lean4_code	字符串	完整可运行的 Lean 4 代码
has_proof	布尔值	如果包含真实证明（非 sorry）则为 True
proof_body	字符串（可选）	证明策略块（如果 has_proof 为真）
natural_language	字符串（可选）	自然语言问题陈述（如果可用）
lean_version	字符串（可选）	原始 Lean 工具链版本
split	字符串（可选）	train/test/val 分割
tags	字符串列表	标签（主题、难度等）
category	字符串（可选）	数学类别
verification	字符串（JSON）	每个 Lean 版本的完整验证结果
v4210_is_valid	布尔值（可选）	True=有效, False=错误/sorry, None=超时
v4210_compiles	布尔值	代码是否编译（is_valid 不为 None）
v4210_has_sorry	布尔值（可选）	是否检测到 sorry
v4210_latency_s	浮点数（可选）	验证挂钟时间（秒）

验证信息

• 所有问题均已针对 Lean-server v4.21.0 在 UVA 的 HPC 集群上进行了验证。
• 验证结果以结构化的 verification JSON 列和平坦化的便捷列形式嵌入每一行。
• verification 列包含一个 JSON 字符串，映射 Lean 版本到结果。

搜集汇总

数据集介绍

构建方式

在形式化数学与定理证明领域，ai4math-lean数据集通过整合21个独立的Lean 4形式数学数据集构建而成。其构建过程涵盖了从多个公开来源系统性地收集数学问题与证明代码，包括竞赛题目、教材习题及研究项目中的形式化陈述。每个问题均经过严格的机器验证，使用lean-server v4.21.0在高效能计算集群上执行编译与正确性检查，确保代码的可靠性与一致性。验证结果以结构化JSON和扁平化字段两种形式嵌入数据行，为后续分析提供了完整的技术追溯。

特点

该数据集的核心特征在于其规模宏大且标注精细，总计包含超过三百万个数学问题，其中约一百二十七万附带完整证明。每个数据条目均包含形式化陈述、可执行的Lean 4代码、自然语言描述及多维度元数据，如数学类别与难度标签。尤为突出的是，数据集嵌入了基于Lean 4.21.0版本的验证状态标识，明确区分有效证明、编译通过但含占位符的代码以及验证超时等情况。这种设计使得数据集不仅适用于监督学习，也为强化学习场景中证明补全任务提供了理想素材。

使用方法

使用该数据集时，研究者可通过HuggingFace的datasets库便捷加载特定子集或启用流式传输以处理海量数据。典型应用包括筛选已验证的有效证明用于模型微调，或提取编译成功但缺乏完整证明的条目作为强化学习训练目标。数据集中丰富的字段如formal_statement、lean4_code和natural_language支持多模态任务设计，而验证状态字段允许直接过滤高质量样本，从而构建稳健的训练与评估基准，推动形式化数学自动化研究的发展。

背景与挑战

背景概述

形式化数学与定理证明领域长期致力于将数学推理转化为可被计算机严格验证的代码，以提升数学研究的严谨性与自动化水平。ai4math-lean数据集由研究团队于近期构建并发布，其核心目标在于为基于Lean4交互式定理证明器的机器学习模型提供大规模、高质量的训练与评估资源。该数据集汇聚了来自多个知名数学问题库的逾三百万个形式化问题，涵盖了从基础数学到奥林匹克竞赛级别的广泛内容，旨在推动自动定理证明与形式化数学教育等关键研究方向的发展。

当前挑战

在自动定理证明领域，模型需从形式化陈述中生成或补全机器可验证的证明，这要求模型具备深度的逻辑推理与精确的符号操作能力，其核心挑战在于处理数学陈述的复杂抽象性与证明步骤的漫长搜索空间。数据集的构建过程同样面临显著困难：首先，整合来自不同来源、遵循各异编码规范的形式化数学代码，并确保其在统一Lean4版本下的语法兼容性与语义一致性，是一项繁重的工程任务；其次，对海量代码进行自动化验证以标注其有效性，需要克服计算资源消耗巨大与验证超时等技术瓶颈，以保障数据标签的可靠性。

常用场景

经典使用场景

在形式化数学与定理自动证明领域，ai4math-lean数据集为基于Lean 4交互式定理证明器的机器学习模型提供了核心训练资源。该数据集整合了21个不同来源的形式化数学问题，涵盖从基础代数到奥林匹克竞赛级别的复杂命题。其经典应用场景在于训练能够理解形式化数学语言、生成严谨证明步骤的神经定理证明器。研究人员利用数据集中的结构化字段，如形式化陈述、完整Lean 4代码及机器验证标签，构建端到端的证明生成与补全系统。这些系统通过模仿人类证明策略，逐步推导出符合形式化验证标准的数学证明。

解决学术问题

该数据集有效解决了形式化数学中机器可验证证明的大规模数据稀缺问题。传统数学证明往往依赖自然语言描述，难以被计算机直接理解与验证。ai4math-lean通过提供超过三百万条经过Lean 4严格验证的形式化问题，为定理自动证明研究建立了标准化基准。它使得研究人员能够系统评估模型在形式化推理、证明策略生成和代码合成等方面的能力。数据集中的验证标签进一步区分了可编译代码与完整证明，为监督学习与强化学习提供了精确的训练信号，推动了神经符号推理方法的实质性进展。

衍生相关工作

围绕ai4math-lean数据集，已衍生出多项具有影响力的研究工作。DeepSeek-Prover系列模型利用该数据集进行预训练，在形式化数学基准测试中取得了突破性性能。Goedel项目通过整合数据集中的问题集合，构建了大规模定理证明环境，用于探索强化学习在证明搜索中的应用。ProofNet等基准测试集进一步扩展了数据集的评估维度，建立了跨领域的形式化数学推理基准。这些工作共同推动了神经定理证明领域的发展，使模型能够处理更复杂、更抽象数学概念的自动证明，为数学知识的形式化与自动化奠定了坚实基础。