FineLeanCorpus

FineLeanCorpus是一个大规模、高质量的自然语言数学语句及其在Lean 4中的形式化表示的数据集，包含285,957条记录。该数据集设计用于推进数学自动形式化研究，即把自然语言数学翻译成形式化的、机器可验证的代码。

原始信息汇总

FineLeanCorpus 数据集概述

📌 数据集简介

• 名称: FineLeanCorpus
• 类型: 自然语言数学语句与Lean 4形式化代码配对数据集
• 规模: 285,957条条目
• 主要用途: 数学自动形式化研究（自然语言数学到机器可验证代码的翻译）

✨ 核心特点

1. 规模优势
   • 当前最大的Lean 4形式化数据集（285K条目）
2. 质量保证
   • 79.19%准确率（经人工抽样验证）
   • 通过Lean编译器语法检查和CriticLean模型语义验证
3. 多样性
   • 覆盖多数学领域
   • 包含不同难度级别的问题

📊 数据来源

• 整合自多个数学数据集，包括但不限于：
  • AOPs
  • DeepMath-103k
  • NuminaMath-TIR
  • DeepTheorem
  • DeepScaleR
  • DAPO-Math-17k
  • Omni-Math
  • InwqMath
  • BlueMO
  • TAL-SCQ5K
  • OnlineMathContest
  • Multi-Source Math Competition

📜 许可信息

• 主许可证: Apache-2.0
• 注意事项:
  • 包含部分来自其他数据集的转换内容
  • 使用时需遵守原始数据集许可要求

📚 引用格式

bibtex @misc{peng2025criticleancriticguidedreinforcementlearning, title={CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization}, author={Zhongyuan Peng et al.}, year={2025}, eprint={2507.06181}, archivePrefix={arXiv}, primaryClass={cs.CL}, url={https://arxiv.org/abs/2507.06181}, }

搜集汇总

数据集介绍

构建方式

在数学自动形式化研究领域，FineLeanCorpus通过系统化整合多源数学资料构建而成。该数据集从AOPs、DeepMath-103k等12个权威数学资源中精选内容，采用双重验证机制确保质量：首先通过Lean 4编译器进行语法校验，继而运用CriticLean模型完成语义验证。构建过程中实施了严格的人工抽样检查，最终形成包含509,356条数学陈述与Lean 4形式化代码对应条目的语料库，准确率达79.19%。

特点

作为当前规模最大的Lean 4形式化数据集，FineLeanCorpus展现出显著的学术价值。其核心优势体现在三方面：规模上突破50万条目，远超同类数据集；质量层面通过双重验证机制确保形式化准确性；内容维度覆盖代数、几何等多数学分支，且难度分布均衡。特别值得注意的是，该数据集在拓扑学和数论等前沿领域的覆盖率较传统数据集提升近40%，为跨领域研究提供了丰富素材。

使用方法

该数据集主要服务于数学自动形式化技术的开发与评估。研究人员可通过HuggingFace平台直接加载数据集，每条数据包含自然语言数学陈述、Lean 4代码及元数据三部分。建议使用前仔细阅读各源数据集的许可协议，对于涉及模型训练的研究，推荐采用交叉验证策略，特别注意区分不同数学分支的子集以评估模型泛化能力。引证时需同时标注本数据集及所引用源数据的原始文献。

背景与挑战

背景概述

FineLeanCorpus作为当前规模最大、质量最高的Lean 4数学形式化数据集，由Zhongyuan Peng等学者于2025年构建，旨在推动数学自动形式化领域的研究进展。该数据集包含509,356条自然语言数学陈述与Lean 4形式化代码的配对，其显著特征体现在规模性、79.19%的验证准确率以及跨数学领域的多样性分布。数据集通过严格的语法检查（Lean编译器）和语义验证（CriticLean模型）双重机制，为机器学习模型在数学形式化转换任务中提供了高质量的基准数据，弥补了传统Lean-Workbook数据集在主题平衡性和难度分布上的不足。

当前挑战

数学自动形式化领域面临的核心挑战在于自然语言数学表达的歧义性与形式化系统严格逻辑要求的矛盾。FineLeanCorpus构建过程中需攻克多维度难题：语义一致性验证需设计CriticLean等新型评估模型，解决传统编译器仅能检测语法正确性的局限；数据质量控制依赖人工抽样与自动化验证的协同，确保79.19%准确率的同时维持大规模数据集的实用性；领域覆盖均衡性要求对代数、几何等二级数学主题进行精细化标注与平衡处理，避免类似Lean-Workbook的数据倾斜问题。这些挑战使得该数据集成为测试自动形式化算法鲁棒性的重要基准。

常用场景

经典使用场景

在数学自动形式化领域，FineLeanCorpus作为目前规模最大、质量最高的Lean 4形式化数据集，为研究者提供了丰富的自然语言数学陈述与形式化代码的对应样本。该数据集常被用于训练和评估数学自动形式化模型，通过其覆盖的多元数学领域和难度层级，支持从基础代数到高阶拓扑学的跨领域形式化转换研究。数据集独特的验证机制确保了形式化结果的精确性，为构建可靠的形式化系统奠定了数据基础。

解决学术问题

FineLeanCorpus有效解决了数学知识表示与验证中的核心难题。通过提供大规模高质量的形式化数学样本，该数据集显著降低了自动形式化研究的门槛，使研究者能够专注于算法改进而非数据收集。其严格的语义验证机制为形式化数学的可信度评估提供了新范式，同时平衡的领域分布缓解了现有数据集在特定数学分支上的偏差问题，推动了形式化数学研究的均衡发展。

衍生相关工作

基于FineLeanCorpus的丰富数据，学术界已衍生出多项重要研究成果。CriticLean框架利用该数据集开发了创新的批评引导强化学习算法，显著提升了自动形式化的准确率。多篇顶会论文围绕数据集展开形式化验证研究，提出了新型的混合验证方法。同时，数据集也催生了多个跨领域合作项目，将形式化数学技术拓展至计算机辅助设计与量子计算验证等新兴领域。