internlm/Lean-Workbook

该数据集包含在Lean 4中形式化的竞赛级数学问题。数据集分为Lean Workbook和Lean Workbook Plus两部分，分别包含57231个和82893个问题。每个问题都提供了自然语言陈述、答案、形式化陈述和形式化证明（如果可用）。这些数据可以支持自动形式化模型的训练和证明搜索。数据集的开源代码和数据链接已提供，测试环境基于Lean v4.8.0-rc1和相同版本的Mathlib4。

This dataset contains competition-level mathematical problems formalized in Lean 4. The dataset is divided into two parts: Lean Workbook and Lean Workbook Plus, which contain 57,231 and 82,893 problems respectively. For each problem, natural language statement, answer, formal statement, and formal proof (if available) are provided. This data can support the training of automated formalization models and proof search. Open-source code and data links for the dataset are provided, and the test environment is based on Lean v4.8.0-rc1 and the same version of Mathlib4.

原始信息汇总

Lean Workbook 数据集概述

数据集描述

• 主题: 竞赛级别的数学问题，使用 Lean 4 形式化。
• 数据量: 包含 57231 个问题的 Lean Workbook 分割和 82893 个问题的 Lean Workbook Plus 分割。
• 内容: 每个问题提供自然语言陈述、答案、形式化陈述和形式化证明（如果可用）。
• 用途: 支持自动形式化模型训练和证明搜索。

环境

• 测试环境: 基于 Lean v4.8.0-rc1 和相同版本的 Mathlib4。

引用

@misc{ying2024lean, title={Lean Workbook: A large-scale Lean problem set formalized from natural language math problems}, author={Huaiyuan Ying and Zijian Wu and Yihan Geng and Jiayu Wang and Dahua Lin and Kai Chen}, year={2024}, eprint={2406.03847}, archivePrefix={arXiv}, primaryClass={cs.CL} }

搜集汇总

数据集介绍

构建方式

该数据集的构建，是以数学竞赛级别的问题为对象，采用Lean 4形式化语言进行描述。数据集包含了57231个Lean Workbook的问题和82893个Lean Workbook Plus的问题，为每个问题提供了自然语言表述、答案、形式化表述以及可选的形式化证明。

特点

本数据集的特点在于其内容的专业性和深度，覆盖了数学竞赛中的高难度问题，并提供了问题从自然语言到形式化表述的完整转换。这不仅有利于自动形式化模型的训练，也为证明搜索提供了丰富的资源。数据遵循apache-2.0协议开源，保证了其使用的灵活性和广泛性。

使用方法

用户可以通过指定Lean v4.8.0-rc1和Mathlib4的相应版本，在测试环境中使用该数据集。同时，数据集的代码和数据均可在HuggingFace平台获取，方便用户进行下载和利用。遵循数据集的使用规范，用户可以高效地进行数学问题的形式化研究和自动化证明探索。

背景与挑战

背景概述

在数学公式自动形式化及证明搜索领域，InternLM/Lean-Workbook数据集的构建标志着重要的进展。该数据集由胡怀远、吴子健、耿一言、王佳宇、林大华和陈凯等研究人员于2024年创建，旨在为Lean 4编程语言提供大规模的数学问题集。数据集涵盖了57231个Lean Workbook问题及82893个Lean Workbook Plus问题，每个问题都提供了自然语言描述、答案、形式化描述及可选的形式化证明。此项工作为自动化数学证明和公式理解的研究提供了宝贵资源，对形式化数学及计算逻辑领域产生了深远影响。

当前挑战

构建InternLM/Lean-Workbook数据集的过程中，研究人员面临了诸多挑战。首先，如何准确地将自然语言描述的数学问题转化为Lean的形式化表述，确保问题与证明的准确性，是一大难题。其次，数据集的构建还需处理规模庞大的问题集，涉及到的数据清洗、格式化及自动化处理均考验着研究团队的技术实力。此外，数据集在支持自动形式化模型训练和证明搜索的同时，还需兼顾Lean环境的兼容性与效率，这对于数据集的实用性和推广性提出了挑战。

常用场景

经典使用场景

在数学与计算机科学领域，InternLM/Lean-Workbook数据集的典型应用场景是作为自动化证明搜索与形式化模型训练的支撑资源。该数据集包含大量竞赛级别的数学问题，并提供了自然语言表述、答案、形式化表述以及可选的形式化证明，为研究人员提供了一手的训练和测试材料。

解决学术问题

此数据集解决了形式化数学问题表述与自动化证明过程中数据稀缺的问题。通过提供大量经过预形式化的数学问题，它极大地促进了数学问题的自动证明技术发展，为人工智能在数学领域的应用奠定了坚实的基础。

衍生相关工作

基于InternLM/Lean-Workbook数据集，研究者们已经开展了一系列相关工作，包括自动化证明算法的研究、数学公式自动生成系统的开发，以及数学问题理解与解答的智能化系统。这些研究进一步推动了数学与计算机科学的交叉融合。