Team Ai
Datasetpublic

alpha-proof-open-source/10-4-alpha-proof-trajectories

10-4 Alpha-Proof Trajectories English · Public trajectory dataset from the 10-4-alpha-proof project: kernel-verified Lean 4 tactic transitions collected by a Python MCTS controller. The first batch (wave_001_fate_m_v001) contains 20 transitions from 20 FATE-M problems, all solved and independently re-verified by the Lean 4 kernel (strict receipt pass). 中文 · 公开轨迹数据集，来自 10-4-alpha-proof 项目：由 Python MCTS 控制器采集、经 Lean 4 内核 独立复验的战术转移（transition）。首批 wave_001_fate_m_v001 含 20 题 × 20 条… See the full description on the dataset page: https://huggingface.co/datasets/alpha-proof-open-source/10-4-alpha-proof-trajectories.

sourceHugging Faceotherupdated 1d agoView on Hugging Face
0likes33downloads
Dataset Card

10-4 Alpha-Proof Trajectories

English · Public trajectory dataset from the 10-4-alpha-proof project: kernel-verified Lean 4 tactic transitions collected by a Python MCTS controller. The first batch (wave_001_fate_m_v001) contains 20 transitions from 20 FATE-M problems, all solved and independently re-verified by the Lean 4 kernel (strict receipt pass).

中文 · 公开轨迹数据集，来自 10-4-alpha-proof 项目：由 Python MCTS 控制器采集、经 Lean 4 内核 独立复验的战术转移（transition）。首批 wave_001_fate_m_v001 含 20 题 × 20 条 transition，全部 solved 且通过严格复验收据（strict receipt）。

目录结构 / Layout

text
catalog.json                        # 批次索引（batch index）
wave_001_fate_m_v001/
  shard-0001.jsonl                  # 20 条 Transition，一行一条（JSON Lines）
  manifest.json                     # 计数 + sha256 + 版本三元组 + policy_version
showcase/
  example-pell.html                 # 示例展示页（Pell 证明：MCTS 会话增量验证可视化）

数据格式 / Schema

每行一个 JSON 对象（Transition，字段与项目训练口径 alphaproof/data/events.py 对齐）：

字段含义
prompt策略输入（含 Lean 证明状态与生成指令的完整提示）
action选择的战术（tactic）
value_target价值目标（-d(s)，d = 剩余步数；终端为 0）
kindproof / disproof / timeout（本批全部为 proof）
solved是否求解成功（本批全部 true）
terminal_verified终端是否经内核复验（本批全部 true）
logprob_old在线支线行为策略 logprob（本批为 null，CE 主线不使用）
reward与 value_target 分离的奖励位（本批为 null）
extra溯源自证：transition_id、problem_id、receipt_id、attempt_id、状态/请求/收据 sha256、token ids 等

快速读取：

python
import json
rows = [json.loads(l) for l in open("wave_001_fate_m_v001/shard-0001.jsonl")]

版本 / Versions

组件版本
Lean4.28.0-rc1
Mathlibv4.28.0-rc1
Reap0090d73c（完整：IQuestLab/reap@0090d73c5f739e4d74000e053b00fd0148ff46aa）
policy_versionshared-wave-001-input（behavior_sha256 68e645ac0427c4ef08633fb249e314f08bac8f285dd4387ac2f21bdfccf85ce9）
base modelREAL-Prover-fe76f68d（sha256 7ffcbbcea4831ce54254a3514dd792d449587a397bcc3303165cdb611275ff84）

版本字段均已取证（项目文档 + 生成 receipts 的 behavior_identity），本批没有 unverified: 字段。

来源与可追溯性 / Provenance

  • —实验：fate_m_20x200_ce_vs_online_v2_7b_20261005（CE 支线），run formal-20x10/wave_001
  • —源文件：runs/formal-20x10/wave_001/ce/update/replay/transitions.jsonl
  • —transitions_sha256 = 688c733e3527692cc1be57b8087a82d5ad8a3b8be25a5a88e7a70d0970b84df7
  • —源 replay manifest sha256 = a6bf02a5152572cf6ee71e0f889327cb217aa7990ff2ffb2ccb5d8fd25ffc863
  • —源 receipts（ce-receipts-through-wave-001.jsonl）sha256 = 0fe96d85953644150bde6e77e253cb6dff23bd92f7243b4dd89619ae7818266a
  • —生成时间：2026-10-05（UTC）；发布：2026-10-09（UTC）
  • —本目录 shard-0001.jsonl 为 lmc-store 导出格式（canonical）（2026-10-09 对齐）： 与源 transitions.jsonl 逐条内容一致、JSON 序列化字节不同；本目录文件 sha256 见 wave_001_fate_m_v001/manifest.json（schema lmc.export_manifest.v1）。
  • —逐文件计数与 sha256 见 wave_001_fate_m_v001/manifest.json

本批 20/20 条来自独立严格复验收据链（verification.result == "verified"，kernel exit 0）。

许可 / License

公开（Public）。 本数据集全部内容公开发布，可自由访问、阅读，并可用于研究与引用。 未声明 SPDX 标准许可证；本仓不代表对上游模型权重的再许可。

Public release. All content is published publicly for research use and citation. No SPDX license is declared; this repo does not relicense any upstream model weights.

引用 / Citation

若使用本数据，请引用本数据集（10-4-alpha-proof 项目，alpha-proof-open-source 组织）：

bibtex
@misc{alpha_proof_104_trajectories,
  title        = {10-4 Alpha-Proof Trajectories},
  author       = {{10-4-alpha-proof project}},
  year         = {2026},
  howpublished = {Hugging Face dataset},
  url          = {https://huggingface.co/datasets/alpha-proof-open-source/10-4-alpha-proof-trajectories}
}