SFT_Dataset

DiffLean SFT 数据集是一个用于在 Lean 4 中对形式化定理证明器进行监督微调的合成数据集。该数据集包含 656,160 个数学问题示例，每个问题都配有形式化陈述和经过验证的 Lean 4 形式化证明。数据集包含六个字段：问题（自然语言描述的数学问题）、来源（原始数据集，如 dart-math-hard）、形式化陈述（Lean 4 形式化陈述）、问题类型（如代数等类别）、形式化证明（经过验证的 Lean 4 形式化证明）和推理。该数据集仅包含训练集，适用于文本生成任务，特别是与定理证明、数学和形式验证相关的应用场景。