lean-eval-source

该数据集为 Lean Eval Humanize Source，提供222个自包含的Lean Eval工作区的可重现快照，这些工作区均使用Humanize工作流进行尝试。每个工作区包含受信任的问题文件（Challenge.lean、Solution.lean）、最佳可用的Humanize提交快照（Submission.lean）以及可选的辅助模块（Submission/）。快照中共有149个被比较器接受的提交，以及73个未接受或未验证的尝试。注意：该数据集仅用于评估，不可用作训练数据，否则会污染基于这些问题的基准测试。数据集的目录结构包括 problems/index.json（包含219个问题记录的索引，字段有id, title, test, submitter, module, holes, generated_path）以及每个问题ID对应的子目录，内含配置文件和构建文件（config.json, lakefile.toml, lean-toolchain）。该数据集适用于形式验证、定理证明和数学领域的评估任务。This dataset is Lean Eval Humanize Source, providing reproducible snapshots of 222 self-contained Lean Eval workspaces, all of which have been attempted using the Humanize workflow. Each workspace contains trusted problem files (Challenge.lean, Solution.lean), the best available Humanize submission snapshot (Submission.lean), and optional auxiliary modules (Submission/). Among the snapshots, there are 149 submissions accepted by the comparator, and 73 attempts that were either not accepted or not verified. Note: This dataset is intended for evaluation only and should not be used as training data, as it would contaminate benchmarks based on these problems. The dataset directory structure includes problems/index.json (an index of 219 problem records with fields: id, title, test, submitter, module, holes, generated_path) and a subdirectory for each problem ID containing configuration and build files (config.json, lakefile.toml, lean-toolchain). This dataset is suitable for evaluation tasks in formal verification, theorem proving, and mathematics.

原始信息汇总

数据集概述

名称：Lean Eval Humanize Source

数据集标识：humanfia-lab/lean-eval-source

许可协议：其他（UNLICENSED，版权所有 © Zijian Zhang）

语言：英语

规模：n < 1K

标签：lean、lean4、形式化验证、定理证明、数学

---

核心内容

该数据集是222个自包含Lean Eval工作区（workspace）的可复现快照，这些工作区均以Humanize工作流进行尝试。每个工作区包含受信任的问题文件、可用的最佳Humanize提交快照，以及任何提交辅助模块。

快照中包含149个通过比较器（comparator）认可的提交，以及73个未认可或未验证的尝试。包含某个尝试并不代表其证明是有效的。

---

使用方法

可通过以下命令下载工作区：

sh hf download humanfia-lab/lean-eval-source --repo-type dataset --include problems/* --local-dir .

在问题目录中，获取依赖并构建：

sh lake update lake build

运行 lake test 还需要Lean Eval文档中规定的比较器工具链。

---

数据结构

problems/ ├── index.json └── <problem_id>/ ├── Challenge.lean ├── Solution.lean ├── Submission.lean ├── Submission/ # 可选辅助模块 ├── config.json ├── lakefile.toml └── lean-toolchain

• Challenge.lean 和 Solution.lean 是受信任的基准文件
• Submission.lean 及 Submission/ 目录下的模块是Humanize尝试的内容
• 每个工作区还附带自己的文档和比较器支持文件
• problems/index.json 描述了来自Lean Eval目录的219个工作区，每个问题包含 id、title、test、submitter、module、holes 和 generated_path 字段
• 其余3个工作区是生成补充，在索引中没有记录

---

来源信息

该快照的清单和来源元数据（包含222个问题的有序列表、149个已接受ID、目录索引和Humanize源记录）存放在 flowbench 内部仓库的 datasets/lean_eval/ 目录下。

---

重要警告

每个工作区都附带一个 Solution.lean 参考证明。该数据集应仅作为评估材料使用，不应作为训练数据：将其包含在预训练或微调语料库中会污染基于这些问题构建的任何基准测试。

搜集汇总

数据集介绍

构建方式

本数据集以Lean Eval基准测试为蓝本，经由Humanize工作流系统性地构建而成，旨在捕捉自动形式化验证中的真实尝试轨迹。每个工作区均包含受信任的问题文件（如Challenge.lean和Solution.lean）、Humanize流程生成的最佳提交快照，以及辅助模块，共计222个自包含工作区。其中，149个提交通过了比较器验证，而73个未获接纳或未能证实。构建过程严格遵循可复现原则，并通过config.json和lean-toolchain等文件锁定环境配置，确保数据集在时间上的稳定性和可追溯性。

特点

该数据集的核心特点在于其双层结构：一方面，它提供了标准化的基准问题（Challenge.lean与Solution.lean），用以评估定理证明器的性能；另一方面，它封存了Humanize流程的原始提交版本（Submission.lean及辅助模块），揭示了自动证明尝试的多样性与局限性。此外，数据集的索引文件（index.json）详尽记录了每项问题的元数据，如模块、洞的数量及生成路径，为深层分析提供了结构化的入口。尤为重要的是，其明确警告该数据集仅用于评估而非训练，以规避数据污染风险，彰显了其科研诚信的坚守。

使用方法

使用者可便捷地通过Hugging Face CLI下载所需工作区，并借助Lake构建系统完成依赖获取与项目编译。每个问题目录内的README与配置文件提供了自解释的构建与测试流程，而运行`lake test`则需配合Lean Eval的官方比较器工具链。数据集的分层组织——从全局索引到具体问题——允许研究者灵活选取子集进行实验，无论是复现Humanize的效果，还是探索新策略在标准难题上的表现，均能无缝接入。其清晰的许可证（UNLICENSED）与出处信息，为合法合规的学术应用奠定了坚实基础。

背景与挑战

背景概述

Lean Eval Humanize Source数据集由Zijian Zhang团队于近期构建，旨在促进形式化验证与定理证明领域的研究。该数据集包含222个自包含的Lean Eval工作区，其中149个通过比较器验收，73个未通过或未验证，每个工作区配有受信任的问题文件与最佳Humanize提交快照。其核心研究问题聚焦于自动化定理证明中Humanize工作流的可复现性与评估基准的纯净性，对推动形式化数学与机器学习交叉领域的发展具有重要影响力。数据集的发布为研究人员提供了标准化的评估材料，助力提升证明搜索算法的鲁棒性与性能。

当前挑战

该数据集面临多重挑战。领域层面，形式化定理证明的自动化程度仍受限于证明策略的搜索空间与复杂数学推理的表示能力，如何构建高效且泛化能力强的证明模型是核心难题。构建过程中，确保工作区的自包含性与依赖管理的准确性极具挑战，需处理Lean工具链版本兼容及环境复现问题。同时，数据集明确警示：若将评估材料混入训练语料，将污染下游基准，因此严格隔离训练与评估数据，维护数据纯净性，成为构建过程中的关键挑战。此外，验收标准（比较器）的制定与统一，以及未验证提交的可信度标记，也需谨慎处理。

常用场景

经典使用场景

在形式化验证与自动定理证明的交叉领域，Lean Eval Humanize Source 数据集为评估大语言模型在 Lean 4 证明生成任务上的能力提供了标准化、可复现的基准。该数据集收录了 222 个自包含的证明工作区，每个工作区均包含经过信任的挑战问题、参考证明及模型提交的快照，并通过统一的配置与工具链支持 `lake build` 与 `lake test` 的自动化验证。研究者可利用该数据集复现 Humanize 工作流的完整评估流程，衡量模型生成证明的正确性与可验证性，从而推动形式化数学与智能证明助手的发展。

衍生相关工作

围绕该数据集，衍生出一系列经典研究，包括基于对比器的证明评估框架优化、证明搜索策略的后处理校准，以及多模型在统一任务上的鲁棒性对比研究。例如，研究者通过 Humanize 工作流对该数据集的 222 个问题进行了系统性尝试，揭示了模型通过“猜测”证明步骤的局限，并进一步开发了基于证明脚本分析的反馈机制。此外，该数据集被用于训练和评估针对 Lean 4 语法与策略调用的嵌入模型，推动了面向形式化证明的预训练语言模型的进步，并为证明助手与 LLM 的混合系统设计提供了实验基石。

数据集最近研究

最新研究方向

该数据集聚焦于形式化验证与机器学习交叉领域的最新进展，具体围绕Lean证明助手生态中的自动化定理证明能力评估。当前研究前沿集中于利用大语言模型（LLM）生成数学证明的可靠性验证，尤其关注在严格形式化环境下模型的推理一致性与策略可复现性。lean-eval-source提供了222个自包含的Lean工作区快照，包含挑战问题、参考证明及多种提交尝试，为评估“人性化”工作流（Humanize）在形式化数学中的应用效果提供了标准化基准。这一资源对于推动自动定理证明系统从非正式推理向严格形式化验证的跨越具有重要意义，同时为构建面向数学领域的鲁棒智能推理系统提供了关键测试床，其设计也警示了数据污染对基准评估的潜在威胁，凸显了构建纯净评估集的前瞻性考量。