Lean 4 sub-goal (gap) dataset harvested from natural-language draft → Lean
sketch → real-Lean goal-state extraction over the
NuminaMath-LEAN
formal statement pool, gated for Lean 4.27.0. Each row is one open
hole (sorry) inside a sketch, paired with the Lean goal-state recorded at
that hole during sketch extraction, suitable as a per-sub-goal prove-step
training signal.
This is the augmented-training complement to
NuminaMath-LEAN-satp-v4.27:
where… See the full description on the dataset page:
https://huggingface.co/datasets/ChristianZ97/NuminaMath-LEAN-satp-gaps-v4.27.
