LeanWorkbook-filtered

该数据集包含四个字段：问题ID（problem_id），非正式陈述（informal_statement），正式陈述（formal_statement）和领域（domain）。数据集的训练集部分含有40076个示例，总大小为14449278字节。数据集适用于机器学习模型的训练，特别是在自然语言处理和文本理解方面。

原始信息汇总

数据集概述

基本信息

• 数据集名称: IMO-Prover/LeanWorkbook-filtered
• 下载大小: 6,142,847字节
• 数据集大小: 14,449,278字节

数据集特征

• problem_id: 字符串类型，表示问题的唯一标识符
• informal_statement: 字符串类型，表示问题的非形式化描述
• formal_statement: 字符串类型，表示问题的形式化描述
• domain: 字符串类型，表示问题所属的领域

数据划分

• 训练集 (train):
  • 样本数量: 40,076
  • 字节大小: 14,449,278字节

配置文件

• 默认配置 (default):
  • 数据文件路径: data/train-*

搜集汇总

数据集介绍

构建方式

LeanWorkbook-filtered数据集作为形式化数学领域的专业语料库，其构建过程体现了严谨的学术规范。研究团队从Lean定理证明器中系统性地提取数学命题，通过自动化流程将每个命题的非形式化描述与形式化表述精准配对。数据集覆盖多个数学领域，每个条目均标注明确的领域标签和唯一的问题标识符，确保数据结构的完整性和可追溯性。原始数据经过多重质量过滤机制，剔除重复和低质量样本，最终形成包含40,076个高质量样本的训练集。

特点

该数据集最显著的特征在于其独特的双模态表述结构，每个数学命题同时包含自然语言描述和形式化语言表达，为研究数学语言的形式化转换提供了理想素材。数据涵盖代数、几何、拓扑等多样化数学分支，domain字段的精细标注支持领域特定的研究需求。样本规模达到四万余条，具有足够的统计显著性，而严格的质量控制保证了命题表述的准确性和一致性，特别适合机器学习模型学习数学概念的抽象表征。

使用方法

研究者可通过HuggingFace平台直接加载该数据集，默认配置自动加载完整的训练分割。数据集采用标准的键值对结构，problem_id字段提供唯一索引，informal_statement和formal_statement字段构成核心研究材料。典型应用场景包括但不限于：形式化数学语言的自动生成、数学文本的形式化转换模型训练、跨领域数学命题的特征分析等。使用时应特别注意保持训练集的原生分布，以充分利用其领域标注的监督信息。

背景与挑战

背景概述

LeanWorkbook-filtered数据集聚焦于数学定理的形式化与自然语言表述之间的转换问题，由专注于形式化数学研究的团队在近年构建完成。该数据集收录了四万余条数学命题的非形式化描述与形式化表述对照样本，覆盖多个数学领域，旨在为形式化数学与自然语言处理交叉研究提供结构化资源。其核心价值在于弥合数学家直觉表达与计算机可处理形式语言之间的鸿沟，为自动定理证明、数学知识库构建等前沿方向奠定数据基础，显著推动了形式化数学的可扩展性研究。

当前挑战

该数据集首要解决形式化数学表述的标准化难题，需克服数学概念在不同抽象层级间的精确映射挑战，这对语义一致性校验机制提出极高要求。数据构建阶段面临双重压力：一方面，专业数学知识的标注依赖领域专家，导致质量控制与规模扩展存在天然矛盾；另一方面，形式化语句的语法约束与自然语言表达的灵活性之间存在显著差异，需设计复杂的中间表示框架来协调二者。这些特性使得数据清洗和跨域泛化成为持续性的技术瓶颈。

常用场景

经典使用场景

LeanWorkbook-filtered数据集在形式化数学领域具有重要价值，其经典使用场景主要集中在数学定理的自动证明和形式化验证。该数据集通过提供大量非形式化陈述与形式化陈述的对应关系，为机器学习模型学习数学语言的形式化转换提供了丰富素材。研究人员可以基于该数据集训练模型，实现从自然语言描述的数学问题到形式化语言表达的自动转换，这在数学辅助证明系统开发中尤为关键。

解决学术问题

该数据集有效解决了形式化数学领域的两大核心问题：一是弥补了自然语言数学描述与形式化语言之间的语义鸿沟，为跨模态数学表达研究提供了基准数据；二是缓解了形式化数学数据稀缺的困境，支持数据驱动的定理自动证明方法研究。其意义在于推动了数学知识表示学习的发展，为构建智能数学辅助系统奠定了数据基础。

衍生相关工作

基于该数据集已衍生出多项重要研究，包括形式化数学语言的神经机器翻译模型、基于注意力机制的定理证明辅助系统，以及数学陈述的自动形式化转换框架。这些工作显著推进了自动推理领域的发展，其中部分成果已被整合到Lean定理证明器等开源工具中，形成了良性的研究生态。