LeanTransitionCorpus
收藏资源简介：
LeanTransitionCorpus 是一个增量发布的存档 Lean 证明过渡数据集，旨在为机器学习研究提供 Lean 定理证明过程中的状态过渡数据。该数据集从 Numina 项目批次中提取，每个样本对应一个证明步骤（过渡），包含从证明前状态到证明后状态的信息。数据采用 Zstandard 压缩的 Parquet 分片格式存储，每行包含 40 列，涵盖 schema_version、step_index、terminal、imports、atomic_tactics、used_premises、available_context 等字段，以及多个递归/对象列（如 provenance、state_before_structured、state_after_structured 等），这些列以 JSON 文本形式存储，保留完整的 Lean 树结构。数据集包含三个子集：训练集（11,182 行）、开发集（654 行）和内部测试集（1,269 行），总计 13,105 个过渡行，对应 1,374 个源不同的证明。每个样本具有全局唯一且确定的 example_id，基于版本化的 SHA-256 身份。该数据集适用于 Lean 证明状态预测、证明策略生成等任务，但注意部分样本的 replay_status 为 not_run，未经过独立 Lean 重放验证。
LeanTransitionCorpus is an incrementally released archived Lean proof transition dataset, designed to provide state transition data during the Lean theorem proving process for machine learning research. The dataset is extracted from the Numina project batches, with each sample corresponding to a proof step (transition), containing information from the pre-proof state to the post-proof state. The data is stored in Zstandard-compressed Parquet shard format, with each row containing 40 columns, including fields such as schema_version, step_index, terminal, imports, atomic_tactics, used_premises, available_context, and multiple recursive/object columns (e.g., provenance, state_before_structured, state_after_structured, etc.), which are stored as JSON text preserving the complete Lean tree structure. The dataset consists of three subsets: training set (11,182 rows), development set (654 rows), and internal test set (1,269 rows), totaling 13,105 transition rows corresponding to 1,374 proofs from different sources. Each sample has a globally unique and deterministic example_id based on a versioned SHA-256 identity. This dataset is suitable for tasks such as Lean proof state prediction and proof strategy generation, but note that the replay_status of some samples is not_run, meaning they have not been independently verified by Lean replay.
LeanTransitionCorpus 数据集详情
基本信息
- 许可证: MIT
- 数据集结构: 包含三个配置（split），分别为
train、dev和internal_test，数据以 Zstandard 压缩的 Parquet 分片格式存储。
数据内容与格式
- 数据粒度: 每一行代表一个 Lean 证明转换步骤（transition）。
- Schema 版本:
leangpt-parquet-v2，共 40 列全部保留。 - 列类型:
- 整数列（int64）：
schema_version、step_index - 布尔列：
terminal - 字符串列表：
imports、atomic_tactics、used_premises、available_context - 其余列均为可空字符串。
- 整数列（int64）：
- 递归/对象列: 以下列包含无损 JSON 文本，需用
json.loads解析（非空时）：provenance、source_start、source_end、state_before_structured、state_after_structured、state_before_internal、state_after_internal、tactic_internal。空对象存储为 JSON 字符串{}，空值保持为 null。 - 数据唯一性: 每个转换行的
example_id全局唯一且确定，由基于 provenance 的 proof key 与step_index的版本化 SHA-256 生成，前缀为ltc-v2:。
数据划分统计（本地种子快照）
| Split | 转换行数 | 来源不同的证明数 |
|---|---|---|
| train | 11,182 | 1,159 |
| dev | 654 | 65 |
| internal_test | 1,269 | 150 |
- 种子来源: 285 个 Numina 批次，1,425 个尝试证明，1,378 个提取证明，1,374 个来源不同的证明，最终保留为 13,105 个转换行。
- 排除记录: 有 4 个提取的证明在规范化过程中未能通过内部状态验证，已在批次证据中记录。
- 隔离数据: 本种子中无可疑隔离（quarantine）转换行；所有转换行的
replay_status=not_run。 - 审计结果: 本地审计未发现重复的 provenance 转换键或跨 split 的定理指纹冲突，但此检查不代表独立的 Lean 重放验证。
读取方式
- 推荐使用不可变的 commit SHA 指定
revision进行实验，仓库会随时间增长。 - 支持流式读取（streaming=True）。
证明身份标识
- 通过
proof_id保留来源标识符，但可能被不同的 Numina 选择重复使用。 - 唯一识别一个证明需使用组合键：
(source_dataset, repo_commit, file_path, provenance.source_sha256, provenance.theorem_ordinal, theorem_name)。 - 批次清单（
manifests/batches/）记录验证过的分片哈希/修订、原始批次指纹、提取证据、保留的 proof ID 和基于 provenance 的 proof key。批次清单仅在所有对应分片验证通过后生成。
其他说明
- 原始来源的许可证与限制仍然适用，本数据卡的 MIT 许可证不替代来源语料库的许可条件。
- 若存在隔离文件（
data/quarantine/），其默认不包含在配置中，仅作为存档证据，不视为干净训练样本。
