HyperCactus0/LeanTransitionCorpus

LeanTransitionCorpus

LeanTransitionCorpus is a dataset for training and studying automated theorem proving systems in Lean. Its unit of data is one tactic transition: the proof state before a tactic, the tactic that was executed, and the resulting state. This makes it suitable for tactic prediction, proof-state representation learning, premise selection, retrieval, verification, and trajectory-level training.

Many Lean datasets expose a theorem, tactic, and pretty-printed goal strings. This corpus retains those human-readable views, but also preserves richer information from Lean's elaborator: the tactic Syntax tree, resolved identifiers, recursive Lean Expr trees, local context, metavariables, universe metavariables, source ranges, and premise/context information. The extra representations make it possible to investigate models that use Lean's internal structure rather than recovering it from printed text.

Original source and environment provenance are retained per row. The repository's Apache-2.0 metadata applies to this packaging; source corpus licenses and restrictions remain applicable and are not replaced by this card.

Source datasets

The extraction pipeline draws from pinned snapshots of the following Lean sources. Rows identify their origin in source_dataset, source_url, repo_commit, and toolchain columns.

The extraction uses immutable source revisions: Numina seed 1c12b9b8d6425f3c531c70601b1e70ccb5bc1e6a, DeepSeek-Prover 1ee889f608fb12ba3596757ee91a60acd663ea81, Goedel Lean Workbook b731852af8d8ab11498fda27bce9020738c01c59, Mathlib 29dcec074de168ac2bf835a77ef68bbe069194c5, and OProver/OProofs 3bae0c06157639c0a673679635c669d19c99e906. The Numina seed is retained in this repository as a frozen source snapshot so the packaged rows remain reproducible.

How the data is produced

For each selected theorem, the extractor runs the matching pinned Lean and Mathlib environment, records the sequence of tactic-state transitions, and canonicalizes the result into one row per transition. It validates internal-state structure and continuity between adjacent transitions, assigns deterministic splits, and keeps provenance needed to trace a row back to its source theorem and environment.

Rows are written as Parquet shards. Before publication, every shard is checked against its source rows; uploaded bytes are read back and verified at an immutable Hugging Face revision. Batch manifests record shard hashes, source-batch identity, and extraction evidence.

Evaluation contamination and quarantine

The clean splits are intended for training and analysis, not for preserving benchmark answers. Before publication, source provenance and canonicalized theorem statements are compared with a frozen registry of common Lean benchmarks, including miniF2F, LeanDojo held-out splits, ProofNet, PutnamBench, FIMO, ProverBench, and MathOlympiadBench. Exact source, statement, expression-fingerprint, and provenance matches are excluded. Near-duplicate statement matches are flagged for review rather than silently treated as independent training examples.

Records that trigger these checks are quarantined during extraction and are not part of the published train, dev, or internal_test splits. This policy is applied before split assignment so that structurally equivalent theorems cannot cross between clean splits.

Format

Zstandard-compressed Parquet shards, one row per transition. The physical encoding is leangpt-parquet-v3 with 31 columns. step_index is int64; terminal is boolean; imports and available_context are lists of strings. Other columns are nullable strings.

The following recursive/object columns contain lossless JSON text (parse with json.loads when non-null): provenance, source_start, source_end, state_before_structured, state_after_structured, state_before_internal, state_after_internal, and tactic_internal. This prevents inference from truncating recursive Lean trees or creating incompatible schemas between shards. Null stays null; an empty object stays the JSON string {}.

example_id is globally unique and deterministic. It is the versioned SHA-256 identity of the provenance-based proof key plus step_index, prefixed by ltc-v2:. The earlier colliding source IDs are not retained in another column.

Schema in plain language

Each row is a single ordered step within a proof. The fields fall into these groups:

The recursive structures are stored as lossless JSON strings in Parquet. Parse them with json.loads when you need their tree structure; leave them as strings for text-only training baselines.

Each shard is round-trip checked against its source records before publication, and uploaded bytes are verified at an immutable Hugging Face revision. Split assignments and provenance are retained so experiments can be reproduced and results can be traced back to their source theorem and environment.

Read

from datasets import load_dataset
import json

data = load_dataset(
    "HyperCactus0/LeanTransitionCorpus",
    revision="<immutable commit SHA>",
    split="train",
    streaming=True,
)
row = next(iter(data))
state = json.loads(row["state_before_internal"]) if row["state_before_internal"] else None

Use an immutable revision for experiments. The repository grows over time.

Identity

example_id is globally unique and deterministic. proof_id retains the source identifier and may be reused by distinct Numina selections. Identify a proof by (source_dataset, repo_commit, file_path, provenance.source_sha256, provenance.theorem_ordinal, theorem_name). Batch manifests expose these tuples as JSON-encoded proof_keys, and the versioned example_id hashes that proof key plus step_index.