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: Source-faithful S-expressions of the goal and every hypothesis, as Lean elaborated them. Normalized S-expressions of the same state, with stable local-context indices suitable for model input. Annotated tactic syntax -- the original tactic's syntax tree with identifier leaves resolved to the constants… See the full description on the dataset page: https://huggingface.co/datasets/jajostrains/Mathlib-Normalized-Sexpr.