jajostrains/Mathlib-Normalized-Sexpr

Mathlib Normalized S-Expressions

Lean 4 proof states from Mathlib, paired with the tactic applied at each step, in three representations extracted directly from the Lean kernel:

1. 1.Source-faithful S-expressions of the goal and every hypothesis, as Lean elaborated them.
2. 2.Normalized S-expressions of the same state, with stable local-context indices suitable for model input.
3. 3.Annotated tactic syntax -- the original tactic's syntax tree with identifier leaves resolved to the constants and hypotheses they refer to.

Row identity follows `cat-searcher/leandojo-benchmark-4-random`, so split and row_index join directly against it and the val/test splits remain comparable to published results on that benchmark.

Unlike pretty-printed proof states, S-expressions carry the elaborated term structure: implicit arguments, instance resolution, and binder structure are all explicit, which is what makes graph- and pointer-based models possible.

Loading

from datasets import load_dataset
import json

ds = load_dataset("jajostrains/Mathlib-Normalized-Sexpr", split="train")
row = ds[0]
print(row["model_goal_sexp"])

# Nested payloads are JSON strings; see the schema note below.
syntax_tree = json.loads(row["source_syntax"])
context = json.loads(row["local_context"])

Coverage

Read this before training on the `train` split.

A row is published only when all three representations were extracted and validated for it. Rows are missing for two distinct reasons, and the difference matters:

• —Environment limits -- a source file that did not elaborate within the timeout. These rows are absent for incidental reasons and are, in principle, recoverable. Their absence is close to random.
• —Extractor limits and row data -- most importantly goal_cardinality: this extractor records states with exactly one pending goal, so every tactic invoked against multiple goals is excluded. Their absence is systematic.

Known bias

The train split is not a uniform random subsample of its upstream split. Because multi-goal invocations are excluded by construction, single-goal proof states are over-represented relative to the full benchmark, as are the tactics that tend to be applied to them. Any comparison against a model trained on all upstream rows should account for this.

The val and test splits are near-complete, so evaluation numbers computed on them remain comparable with published results.

Per-split failure taxonomy

test -- 114 rows not published

train -- per-phase breakdown unavailable

This split was extracted over several runs, and the manifest left on disk covers only 3,000 of its 250,814 rows. Rather than report phase counts measured on that fraction as if they described the split, they are omitted. The aggregate coverage above is measured from the published rows themselves and is exact; the causes listed under Coverage all apply here, goal_cardinality and file_compile foremost, but their relative sizes for this split are not established.

val -- 103 rows not published

Schema

All three representations for a row ship in that same row, so nothing needs to be joined across files. Recursive payloads (source_syntax, local_context, the hypothesis lists) are stored as JSON strings: their shape varies per tactic, and a typed nested column would force either schema inference failures or a lowest-common-denominator union. Call json.loads on them.

Provenance

• —Mathlib commit: 29dcec074de168ac2bf835a77ef68bbe069194c5
• —Upstream dataset: cat-searcher/leandojo-benchmark-4-random
• —Extraction: each Mathlib source file is elaborated with a patched Pantograph REPL, and the proof state Lean records at each matched tactic invocation is captured. States are read from Lean, never parsed back from pretty-printed text.
• —test: extractor lean-action-trace-v3, raw schema v3, Pantograph unknown
• —train: extractor lean-action-trace-v3, raw schema v3, Pantograph unknown
• —val: extractor lean-action-trace-v3, raw schema v3, Pantograph unknown

Limitations

• —Single-goal states only; see Coverage.
• —train coverage is partial and biased; val/test are near-complete.
• —S-expressions are large. Expect the goal and hypothesis columns to dominate memory; select only the representation you need.
• —Normalized and source-faithful S-expressions are different representations of the same state, not alternatives of equal fidelity. Train on model_*; use raw_* when you need exactly what Lean emitted.

License and attribution

This dataset is released under apache-2.0. It is derived work, and both upstream licenses continue to apply to the material they cover:

• —Mathlib 4 is licensed Apache-2.0. Theorem names, tactic text, file paths, and every elaborated term in the S-expression columns derive from Mathlib at commit 29dcec074de168ac2bf835a77ef68bbe069194c5. See <https://github.com/leanprover-community/mathlib4/blob/master/LICENSE>.
• —LeanDojo is licensed MIT. The row selection and the split / row_index assignment are inherited unchanged from the LeanDojo benchmark, so its notice is reproduced below as MIT requires.

MIT License

Copyright (c) 2023 LeanDojo Team

Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:

The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.

THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.

Citation

Please cite both upstreams alongside this dataset: Mathlib for the mathematical content, and LeanDojo for the benchmark this dataset's row identity follows.