LEAN-GitHub

该数据集包含了从GitHub上几乎所有Lean 4仓库中提取的大规模正式数据，其中包含28,597个带有形式证明的定理和218,866个策略，这些数据来自2,133个文件。该数据集是Lean 4形式数学中最大的定理证明数据集之一，对于提高模型在各类数学主题上的性能具有显著益处。其规模达到0.138B个标记，任务是对形式数学中的定理进行证明。

This dataset comprises large-scale formal data extracted from nearly all Lean 4 repositories on GitHub. It includes 28,597 theorems with formal proofs and 218,866 tactics, sourced from 2,133 files. As one of the largest theorem-proving datasets in Lean 4 formal mathematics, it offers substantial benefits for enhancing model performance across various mathematical topics. The dataset has a scale of 0.138 billion tokens, with its core task being theorem proving in formal mathematics.