datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
NuminaMath-LEAN-Sol
NuminaMath-LEAN Cleaned with NL Solutions
Dataset Summary
This is a cleaned version of the NuminaMath-LEAN dataset, enhanced with natural language (NL) solutions matched from source datasets. The primary goal is to provide paired formal statements/proofs with natural language solutions for proof formalization and theorem proving research.
The dataset matches problems from NuminaMath-LEAN with their corresponding natural language solutions from:
olympiads-ref: A… See the full description on the dataset page: https://huggingface.co/datasets/iiis-lean/NuminaMath-LEAN-Sol.2026-08-02-qwen36-mixture-500k-numina-heavy-empty-think
Qwen3.6-27B SFT mixture — 500k maths-weighted, empty-think markers
499,595 tokens across 1,001 conversations, weighted toward maths, with Qwen3.6's empty
think marker on the non-maths rows. md5 c433f31eba2b5b4919fb166043caccb5.
Source
Examples
Tokens
Share
Marker
NuminaMath-CoT
611
333,351
66.9%
no
No Robots
271
82,239
16.5%
yes
TULU3
119
82,445
16.5%
yes
Total
1,001
499,595
390 marked
Derived from
qwen3.6-27b-mixture-500k-numina-heavy
by adding the… See the full description on the dataset page: https://huggingface.co/datasets/dougalldeepmind/2026-08-02-qwen36-mixture-500k-numina-heavy-empty-think.NuminaMath-1.5-Pro
NuminaMath-1.5-Pro
Dataset Overview
NuminaMath-1.5-Pro targets post-training and verifiable reasoning scenarios. It applies strict filtering, judge-based consistency checks, and staged solution regeneration on top of the upstream NuminaMath-1.5 dataset.
All data processing and synthesis for this dataset is executed with the BlossomData framework, covering the full pipeline—loading, filtering, judging, generation, retry, and export—with an emphasis on reproducibility… See the full description on the dataset page: https://huggingface.co/datasets/Azure99/NuminaMath-1.5-Pro.AI-MO-NuminaMath-TIR-korean-240918
IMPORTANT NOTE
This data is part of the progress. Current translation progress: 24.85% (2024-09-18 01:32 KST)
I'm taking a short break due to personal reasons. I'll be back in a month.
TODO-LIST
Finish translation
Translation
I used gemini-1.5-pro-exp-0827. The prompt used for translation will be disclosed at the end.
Dataset Card for NuminaMath CoT
Dataset Summary
Tool-integrated reasoning (TIR) plays a crucial role in this… See the full description on the dataset page: https://huggingface.co/datasets/ChuGyouk/AI-MO-NuminaMath-TIR-korean-240918.GAR_baseDataset_NuminaMath
GAR-Official
This is the official repository for the paper GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving.
GitHub Repository: RickySkywalker/GAR-Official
Trained Models:
GAR_Goedel-Prover-V2
GAR_DeepSeek-Prover-V2
Base Datasets:
Original base dataset
Base dataset under Numina-Math
Introduction
We introduce GAR: Generative Adversarial Reinforcement Learning, an RL training method that intends to solve inefficiency and suboptimal… See the full description on the dataset page: https://huggingface.co/datasets/RickyDeSkywalker/GAR_baseDataset_NuminaMath.NuminaMath-1.5-EFA-Subset📃 Paper
This dataset contains EFAs inferred for a subset of NuminaMath_CoT, specifically the first 5,000 problems.
These EFAs were inferred by this model, and the prompts used for training are linked in the model card.
The dataset contains multiple EFA candidates for most of the first 5,000 problems in NuminaMath.
Each row in the dataset is described by the Row class below:
from pydantic import BaseModel
class ProblemVariant(BaseModel):
"""Synthetic problem variants constructed by… See the full description on the dataset page: https://huggingface.co/datasets/codezakh/NuminaMath-1.5-EFA-Subset.openthoughts3_numinamath-1.5-pro_mixturenumina_smoltalk_mixture