xu3kev/proof-pile-2-proofsteps

---
configs:
- config_name: default
data_files:
- split: lean_proofsteps
path: "lean_proofsteps/*.parquet"
- split: isa_proofsteps
path: "isa_proofsteps/*.parquet"
---

Proofsteps data from Proof-Pile-2

includes proofsteps for Lean and Isabelle

```python
from datasets import load_dataset
ds = load_dataset(
"xu3kev/proof-pile-2-proofsteps"
)

ds
DatasetDict({
lean_proofsteps: Dataset({
features: ['text', 'meta'],
num_rows: 3432
})
isa_proofsteps: Dataset({
features: ['text', 'meta'],
num_rows: 260726
})
})
```

Quoting from appendix of [LLEMMA: AN OPEN LANGUAGE MODEL FOR MATHEMATICS](https://arxiv.org/pdf/2310.10631.pdf)

```
B.1.2 LEAN PROOFSTEPS
We extract a dataset of (tactic state, next tactic) pairs from Mathlib 4 (mathlib Community, 2020)
using the lean-training-data (Morrison, 2023) tool. We use Mathlib 4 commit c779bd5,
which was created on August 20th 2023.
B.1.3 ISABELLE PROOFSTEPS
We construct a dataset of Isabelle proofs, building upon the PISA dataset Jiang et al. (2021). Isabelle
Proofsteps comprises proofs from the Archive of Formal Proofs and Isabelle Standard Library, scraped
with PISA Jiang et al. (2021). Each entry in the dataset includes the theorem statement, the proof
states and the proof steps, separated by specific tags. To maintain the integrity of evaluations using
the PISA test set, we decontaminate Isabelle Proofsteps by removing theorems whose names overlap
with those in the PISA test set. Although this approach results in a strict filtering – removing more
than 10,000 theorems although there are only 3600 in the PISA test set – we consider it acceptable in
order to mitigate data contamination. After filtering, Isabelle Proofsteps contains 251,000 theorems.
```

---
配置项：
- 配置名称：default
数据文件：
- 拆分集：lean_proofsteps
路径："lean_proofsteps/*.parquet"
- 拆分集：isa_proofsteps
路径："isa_proofsteps/*.parquet"
---

本数据集源自Proof-Pile-2，涵盖Lean与Isabelle两种形式化证明框架的证明步骤数据。

python
from datasets import load_dataset
ds = load_dataset(
"xu3kev/proof-pile-2-proofsteps"
)

ds
DatasetDict({
lean_proofsteps: Dataset({
features: ['text', 'meta'],
num_rows: 3432
})
isa_proofsteps: Dataset({
features: ['text', 'meta'],
num_rows: 260726
})
})

本段内容引自《LLEMMA：面向数学的开源大语言模型（LLEMMA: AN OPEN LANGUAGE MODEL FOR MATHEMATICS）》的附录部分：

### B.1.2 Lean证明步骤
我们从Mathlib 4（mathlib社区，2020）中提取（策略状态，下一策略）对数据集，所用工具为lean-training-data（Morrison等，2023）。本次实验使用的Mathlib 4提交版本为c779bd5，创建于2023年8月20日。

### B.1.3 Isabelle证明步骤
我们基于PISA数据集（Jiang等，2021）构建了Isabelle证明数据集。Isabelle证明步骤数据集涵盖来自形式化证明档案库（Archive of Formal Proofs）与Isabelle标准库的证明内容，通过PISA工具（Jiang等，2021）爬取得到。该数据集的每条数据均包含定理陈述、证明状态与证明步骤，通过特定标签进行分隔。为保证基于PISA测试集的评估结果的公正性，我们对Isabelle证明步骤数据集进行了去污染处理：移除所有与PISA测试集中重名的定理。尽管该过滤规则较为严格——尽管PISA测试集仅包含3600条定理，却移除了超过10000条定理，但为了缓解数据污染问题，该处理方式是可接受的。过滤完成后，Isabelle证明步骤数据集共包含251000条定理。

原始信息汇总

数据集概述

数据集名称

Proof-Pile-2-Proofsteps

数据集来源

从Mathlib 4和Isabelle的证明步骤中提取。

数据集内容

数据集包含两个部分：

• lean_proofsteps: 包含3432条记录，每条记录包含text和meta两个特征。
• isa_proofsteps: 包含260726条记录，每条记录包含text和meta两个特征。

数据集描述

• lean_proofsteps: 从Mathlib 4中提取的(tactic state, next tactic)对，使用lean-training-data工具。
• isa_proofsteps: 从Archive of Formal Proofs和Isabelle Standard Library中提取的Isabelle证明步骤，使用PISA工具进行数据清洗，去除了与PISA测试集重叠的定理，最终包含251,000个定理。

数据集加载

python from datasets import load_dataset ds = load_dataset("xu3kev/proof-pile-2-proofsteps")

搜集汇总

数据集介绍

构建方式

在数学定理证明的自动化进程中，高质量的训练数据集是推动模型能力提升的关键基石。该数据集源自Proof-Pile-2项目，专注于收集Lean与Isabelle两种形式化证明系统中细粒度的证明步骤（proofsteps）数据。对于Lean部分，研究者利用lean-training-data工具，从Mathlib 4库（提交版本c779bd5，日期为2023年8月20日）中提取了（策略状态，下一策略）的配对序列。而Isabelle部分则在PISA数据集基础上构建，涵盖了Archive of Formal Proofs与Isabelle标准库中的证明，每条记录包含定理陈述、证明状态及步骤，并通过特定标签分隔。为保障评估的纯净性，研究者对Isabelle Proofsteps进行了严格去污染处理，剔除与PISA测试集定理名称重叠的条目，尽管这导致超过10,000个定理被移除，但有效维护了数据完整性。

特点

该数据集具备显著的领域专业性与结构化特征。在规模上，Lean Proofsteps包含3,432条记录，Isabelle Proofsteps则高达260,726条，为训练大型语言模型在形式化数学推理任务上提供了丰富的样本。每条数据均包含'text'与'meta'两个字段，前者承载证明步骤的具体内容，后者携带元信息，便于研究者深入分析与筛选。数据集的构建严格遵循了数学定理证明的格式规范，尤其是Isabelle部分通过去污染处理，避免了与测试集的潜在重叠，增强了其在模型评估中的可靠性。这种细粒度的步骤级数据，相较于完整的证明文本，更能有效引导模型学习策略选择的逻辑链条。

使用方法

研究者可通过Hugging Face的datasets库便捷地加载该数据集，仅需一行代码即可获取包含'lean_proofsteps'与'isa_proofsteps'两个子集的DatasetDict对象。加载后，每个子集均作为标准的Dataset实例，支持常见的索引、切片与迭代操作。在应用层面，该数据集适合用于训练或微调面向形式化数学证明的序列到序列模型，例如将策略状态映射至下一步策略。研究者可依据'text'字段中的标签结构解析证明步骤，或利用'meta'字段进行条件筛选，如按定理来源或证明阶段划分训练与验证集。对于Isabelle部分，由于已进行去污染处理，可直接用于公平的模型性能评估，无需额外担忧数据泄露问题。

背景与挑战

背景概述

在人工智能与形式化数学交叉领域，定理证明的自动化一直是核心挑战之一。为此，研究人员于2023年构建了Proof-Pile-2-proofsteps数据集，由Kevin Xu等学者依托于LEMMA项目开发，旨在为大型语言模型提供结构化的证明步骤数据。该数据集包含来自Lean和Isabelle两个交互式定理证明器的证明步骤对，其中Lean部分源自Mathlib 4库，基于2023年8月的特定版本提取了约3400条（策略状态，下一策略）对；Isabelle部分则在PISA数据集基础上扩展，涵盖形式化证明档案与标准库，经去污染处理后保留约25万个定理。该数据集填补了数学语言模型在细粒度证明步骤训练数据上的空白，显著推动了面向数学推理的开源语言模型发展。

当前挑战

该数据集面临的核心挑战在于领域问题的复杂性与构建过程的严谨性。在领域层面，定理证明的自动化需处理高度符号化、逻辑严密的数学语言，模型必须理解策略状态与下一步策略之间的因果关联，这对序列建模和推理能力提出了极高要求。构建过程中，Isabelle部分需严格去污染以避免与PISA测试集重叠，尽管采取了移除超过1万个定理的激进过滤策略，仍难以完全消除潜在的数据泄露风险。此外，Lean部分仅含3432条样本，数据规模有限，可能制约模型泛化能力。同时，不同证明器（Lean与Isabelle）的语法和逻辑体系差异，也为跨系统迁移学习带来了额外挑战。

常用场景

经典使用场景

在形式化数学推理与自动化定理证明的交叉领域中，xu3kev/proof-pile-2-proofsteps数据集以其精心构建的（策略状态，下一步策略）二元组结构，成为训练神经定理证明器的经典资源。该数据集整合了Lean和Isabelle两大主流证明助手的证明步骤，其中Lean部分源自Mathlib 4的实战证明轨迹，Isabelle部分则基于PISA数据集扩展并去除了测试集污染。研究者常将其用于训练能够从当前证明状态预测下一步策略的序列模型，从而推动从符号逻辑到神经符号融合的范式演进。

解决学术问题

该数据集有效回应了形式化数学中证明步骤自动生成这一核心学术难题。传统上，定理证明依赖专家手写策略，效率低下且难以规模化。Proofsteps通过提供大规模、高保真的（状态，策略）配对数据，使得深度学习模型能够学习策略选择与状态之间的复杂映射关系，进而自动生成证明步骤。这一突破显著降低了形式化验证的人力成本，并为数学定理的机器辅助证明提供了可复现的基准，其去污染处理更是保障了评估的公正性。

衍生相关工作

该数据集直接催生了多项开创性研究工作，最典型的是LLEMMA语言模型系列。LLEMMA在Proofsteps上微调后，展现出在数学推理任务上的显著能力提升，证明了形式化证明数据对通用数学推理的增益。此外，后续工作如ProofGPT和TacticZero借鉴了其数据构建范式，分别探索了自回归策略生成与强化学习结合的方法。这些衍生工作共同构建了从数据收集到模型训练再到评估的完整闭环，推动了神经定理证明领域的标准化进程。