datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
NuminaMath-LEAN-satp-buffer-dspaug-Temp
NuminaMath-LEAN-satp-buffer-dspaug-Temp
Staging buffer for the DSP+ paper-augmentation sweep (2026-04-29). This
is a -Temp variant — lemma_names / lemma_scores are empty and
theorem_uuid is the join key (matches NuminaMath-LEAN-satp.uuid).
Retrieval population + rename-to-uuid happens at the
promote-to-canonical merge step, mirroring the precedent set by
NuminaMath-LEAN-satp-buffer-planf-v1-Temp.
Why this exists
Schema audit on NuminaMath-LEAN-satp-buffer (40,965… See the full description on the dataset page: https://huggingface.co/datasets/ChristianZ97/NuminaMath-LEAN-satp-buffer-dspaug-Temp.NuminaMath-LEAN-satp-buffer-discard
NuminaMath-LEAN-satp-buffer
Aesop tactic configurations collected during SATP (Steering Aesop for
Theorem Proving) replay-buffer building, paired with the initial Lean
goal_state of each theorem. Each row is one
(theorem, aesop_config) → reward example, intended as positive /
negative replay material for training
SATP-aesop-policy.
Sibling datasets:
NuminaMath-LEAN-satp — main training set (formal_statement → goal_state)
NuminaMath-LEAN-satp-gaps — augmented train set with sub-goal… See the full description on the dataset page: https://huggingface.co/datasets/ChristianZ97/NuminaMath-LEAN-satp-buffer-discard.