SFT_Dataset

Pythagoras SFT 数据集是一个用于定理证明与形式推理的大规模合成数据集，专为基于Lean4的形式化证明任务而设计。该数据集旨在通过提供自然语言问题、对应的Lean4形式化陈述、形式化证明以及推理链，来支持高效的形式证明模型训练。数据集包含约841,000个问题-证明对，当前公开发布了126,000个实例的子集，按难度分为简单（30,000个）、中等（49,000个）和困难（47,000个）三个级别。每个数据实例包含以下字段：自然语言问题描述（Question）、问题来源家族（Source）、Lean4形式化陈述（Formal Statement）、Lean4形式化证明（Formal Proof）、问题所属的广泛数学类别（Problem Type）、证明前的推理链或证明计划（Reasoning Chain）以及难度标签（Difficulty）。该数据集适用于文本生成任务，特别是自动化定理证明、形式推理以及Lean4代码生成等场景。数据生成流程的完整说明可在关联论文《Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation》中找到。

The Pythagoras SFT dataset is a large-scale synthetic dataset for theorem proving and formal reasoning, specifically designed for formal proof tasks based on Lean4. It aims to support efficient formal proof model training by providing natural language problems, corresponding Lean4 formal statements, formal proofs, and reasoning chains. The dataset contains approximately 841,000 problem-proof pairs, with a publicly released subset of 126,000 instances categorized into three difficulty levels: easy (30,000), medium (49,000), and hard (47,000). Each data instance includes the following fields: natural language problem description (Question), problem source family (Source), Lean4 formal statement (Formal Statement), Lean4 formal proof (Formal Proof), broad mathematical category of the problem (Problem Type), reasoning chain or proof plan before proof (Reasoning Chain), and difficulty label (Difficulty). This dataset is suitable for text generation tasks, particularly automated theorem proving, formal reasoning, and Lean4 code generation scenarios. A complete description of the data generation process can be found in the associated paper Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation.

原始信息汇总

数据集概述

基本信息

• 数据集名称：Pythagoras-Prover SFT Dataset
• 语言：英语（en）
• 许可证：Apache-2.0
• 规模：100K < n < 1M
• 任务类别：文本生成（text-generation）
• 标签：Lean4、定理证明、形式推理

数据集内容

该数据集包含约 841K 个问题，每个问题配有：

• Lean 形式化陈述（Formal Statement）
• 形式化证明（Formal Proof）
• 推理链（Reasoning Chain）

当前发布的子集包含 126K 个实例，按难度分为：

• 30K 简单实例（easy）
• 49K 中等实例（medium）
• 47K 困难实例（hard）

完整数据集将后续发布。

数据格式

每一行数据包含以下字段：

• Question：自然语言问题描述
• Source：问题的来源类别
• Formal Statement：Lean 4 形式化表述
• Formal Proof：针对形式化陈述生成的 Lean 4 证明
• Problem Type：数学问题的广义类别
• Reasoning Chain：形式化证明之前的证明计划或推理过程
• Difficulty：难度标签（easy / medium / hard）

示例

一个典型数据条目包含一个组合学问题、其 Lean 4 形式化陈述与证明、推理链，以及难度标签为“easy”。

引用

bibtex @article{leang2026pythagoras, title={Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation}, author={Leang, Joshua Ong Jun and Zhao, Zheng and Stoian, Mihaela Catalina and Xu, Qiyuan and Li, Haonan and Li, Wenda and Cohen, Shay B. and Giunchiglia, Eleonora}, journal={arXiv preprint arXiv:2606.12594}, year={2026} }

相关链接

• 项目主页：https://pythagoras-lm.github.io/
• GitHub 仓库：https://github.com/Pythagoras-LM/Pythagoras-Prover
• 论文：https://huggingface.co/papers/2606.12594

搜集汇总

数据集介绍

构建方式

本数据集源自Pythagoras-Prover项目，旨在推动形式化定理证明领域的发展。其构建采用了一种创新的合成数据生成流水线，通过将自然语言数学问题与Lean 4形式化语言相结合，生成了约84.1万组包含问题、形式化陈述、形式化证明及推理链的配对数据。当前公开发布的子集包含12.6万个实例，依据难度划分为简单（3万）、中等（4.9万）和困难（4.7万）三档。每个实例均经过人工校验与自动化工具的双重验证，确保了数据质量与数学严谨性。

特点

该数据集的核心特点在于其多维度、结构化的数据组织形式。每条记录不仅包含原始自然语言问题，还附带了对应的Lean 4形式化陈述与完整证明代码，以及展示解题思路的推理链。此外，数据集标注了问题的数学领域类别（如组合学、数论等）与难度等级，便于研究者进行针对性的模型训练与评估。这种丰富的信息层次使得数据集既可用于监督学习中的序列生成任务，也能服务于定理证明策略的分析与优化。

使用方法

在使用本数据集时，研究者可将其直接用于文本生成模型的微调，通过自然语言问题作为输入，训练模型输出对应的Lean 4形式化陈述或完整证明。建议将‘Question’字段作为输入序列，‘Formal Statement’或‘Formal Proof’作为目标序列，适用于序列到序列的学习范式。推理链字段则可作为中间监督信号，帮助模型学习逐步推理能力。数据集以标准JSON格式存储，易于加载，且兼容常用的深度学习框架，适合在定理证明、数学推理及代码生成等研究场景中应用。

背景与挑战

背景概述

在形式化数学推理领域，利用大语言模型自动生成Lean等定理证明器可接受的严格形式化证明，已成为人工智能与数学交叉研究的前沿方向。由Joshua Ong Jun Leang、Zheng Zhao、Mihaela Catalina Stoina等研究人员于2026年提出的Pythagoras-Prover项目，针对现有模型在形式化推理中缺乏高质量训练数据的瓶颈，发布了Pythagoras-Prover SFT数据集。该数据集包含约84.1万道问题，配备自然语言描述、Lean4形式化陈述、形式化证明与推理链，覆盖组合数学、数论等多个数学分支，并按照难度划分为易、中、难三个层次。该数据集的构建显著推动了高效形式化证明系统的发展，为提升语言模型在严格数学推理任务中的能力提供了关键基础资源。

当前挑战

在领域问题层面，数据集致力于解决的核心挑战是如何弥合自然语言数学问题与形式化定理证明之间的鸿沟，使模型能够从非形式化表述自主推导出严格、可验证的Lean4证明，这在现有数据稀缺且形式化表达极具精确性的背景下尤为艰巨。在构建过程中，研究人员面临的主要挑战包括：如何设计一个高覆盖率、低噪声的合成数据生成管道，以自动产出大规模、难度层次清晰的同源问题—证明对；如何在保证形式化证明正确性的同时，生成高质量、可读的推理链，以支持模型进行中间步骤的逐步推理；以及如何对实例进行客观的难度标注，确保数据集在训练过程中能有效指导模型由浅入深地掌握形式化证明技巧。

常用场景

经典使用场景

在形式化定理证明与人工智能的交叉领域中，SFT_Dataset（即Pythagoras-Prover SFT数据集）主要被用于训练和评估大语言模型在数学定理形式化及自动证明方面的能力。该数据集包含约12.6万条由自然语言问题、Lean 4形式化陈述、形式化证明及推理链组成的实例，覆盖从组合数学到数论等多个数学分支，难度层次分明。研究者通常利用该数据集对预训练语言模型进行监督微调，使其掌握将非形式化数学问题转化为严格形式化Lean 4代码的方法，并生成可验证的证明脚本，从而为构建端到端的神经形式化证明系统提供高质量的训练资源。

解决学术问题

该数据集的核心学术贡献在于缓解了神经形式化证明领域中高质量、大规模、标注对齐数据匮乏的长期困境。传统上，Lean 4形式化证明的构建高度依赖人类专家，成本极高且难以规模化。通过提供同时包含自然语言问题、形式化陈述、逐步推理链以及完整证明的配对数据，SFT_Dataset使得研究者得以系统性地探索语言模型在“隐式—显式”数学推理链条上的泛化能力。它解决了如何从非结构化文本跳跃到结构化形式化证明的语义鸿沟问题，有力地推动了对数学语言理解、中间推理表示以及正确性验证的联合研究。

衍生相关工作

SFT_Dataset的发布催生了一系列旨在增强定理证明器推理质量与效率的后续研究。例如，受到其多难度分层设计的启发，研究者开发了课程学习策略，让模型首先在简易实例上训练以建立基本语法框架，再逐步过渡至中、高难度样本，从而提升最终形式化证明的生成成功率。另一类工作则聚焦于推理链的利用，探索将数据集中的逐步推理过程作为监督信号，促使模型学习显式的证明规划（proof planning）能力，进而衍生出诸如“形式化—推理链联合训练”或“多任务语义对齐”的方法论。此外，该数据集也被用于评估跨领域零样本转移能力，初步证实了在组合数学和数论上训练得到的模型能够在一定程度上泛化至未曾涉及的数学子领域。