datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
NuminaMath-CoT
Dataset Card for NuminaMath CoT
Dataset Summary
Approximately 860k math problems, where each solution is formatted in a Chain of Thought (CoT) manner. The sources of the dataset range from Chinese high school math exercises to US and international mathematics olympiad competition problems. The data were primarily collected from online exam paper PDFs and mathematics discussion forums. The processing steps include (a) OCR from the original PDFs, (b) segmentation… See the full description on the dataset page: https://huggingface.co/datasets/AI-MO/NuminaMath-CoT.NuminaMath-1.5
Dataset Card for NuminaMath 1.5
Dataset Summary
This is the second iteration of the popular NuminaMath dataset, bringing high quality post-training data for approximately 900k competition-level math problems. Each solution is formatted in a Chain of Thought (CoT) manner. The sources of the dataset range from Chinese high school math exercises to US and international mathematics olympiad competition problems. The data were primarily collected from online exam paper PDFs… See the full description on the dataset page: https://huggingface.co/datasets/AI-MO/NuminaMath-1.5.NuminaMath-1.5-RL-Verifiable
Dataset Card for NuminaMath-1.5-RL-Verifiable
Dataset Summary
NuminaMath-1.5-RL-Verifiable is a curated subset of the NuminaMath-1.5 dataset, specifically filtered to support reinforcement learning applications requiring verifiable outcomes. This collection consists of 131,063 math word problems from the original dataset that meet strict filtering criteria: all problems have definitive numerical answers, validated problem statements and solutions, and come from… See the full description on the dataset page: https://huggingface.co/datasets/nlile/NuminaMath-1.5-RL-Verifiable.NuminaMath-TIR
Dataset Card for NuminaMath CoT
Dataset Summary
Tool-integrated reasoning (TIR) plays a crucial role in this competition. However, collecting and annotating such data is both costly and time-consuming. To address this, we selected approximately 70k problems from the NuminaMath-CoT dataset, focusing on those with numerical outputs, most of which are integers. We then utilized a pipeline leveraging GPT-4 to generate TORA-like reasoning paths, executing the code and… See the full description on the dataset page: https://huggingface.co/datasets/AI-MO/NuminaMath-TIR.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.NuminaMath-LEAN-Proof-Artifacts
NuminaMath-LEAN Proof Artifacts
Dataset Summary
This dataset provides proof-analysis artifacts derived from
AI-MO/NuminaMath-LEAN.
It is released with two aligned configs:
lite: dual-track proof validation/extraction artifacts
full: all lite fields plus dual-track main-theorem structural artifacts
Both configs are aligned by sample identity (uuid, original_index) and processing order.
Config Overview
Use lite for overall tactic usage statistics (e.g.… See the full description on the dataset page: https://huggingface.co/datasets/iiis-lean/NuminaMath-LEAN-Proof-Artifacts.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-v4.27
NuminaMath-LEAN-satp-v4.27
Lean 4 formal-statement + initial proof goal_state pairs over the
NuminaMath-LEAN problem pool, packaged for Lean 4.27.0. This is the main
training set for SATP (Steering Aesop for Theorem Proving) running in a
Lean 4.27 environment.
Every row's formal_statement elaborates cleanly under the pinned toolchain
below, and every goal_state is the pretty-printed goal produced in that
row's own environment — the same rendering the SATP runtime observes at… See the full description on the dataset page: https://huggingface.co/datasets/ChristianZ97/NuminaMath-LEAN-satp-v4.27.NuminaMath-CoT-Small-215k
Summary
This dataset is a scaled down version of the original AI-MO/NuminaMath-CoT dataset.
Source breakdown
Source
Number of Originial Samples
Number of Samples in This Dataset
aops_forum
30201
7548
amc_aime
4072
1017
cn_k12
276591
69138
gsm8k
7345
1835
math
7478
1869
olympiads
150581
37640
orca_math
153334
38328
synthetic_amc
62111
15527
synthetic_math
167895
41968
Total
859608
214870
2026-08-02-qwen36-mixture-100k-tulu-numina-norobots
Qwen3.6-27B SFT mixture — 100k tokens, three sources
99,794 tokens across 211 conversations, in
equal thirds from three instruction-tuning corpora. md5 0ecf29bb97813b8bcf888a4c7f7bf0f6.
Source
Examples
Tokens
Share
no_robots
98
33,254
33.32%
numinamath_cot
64
33,261
33.33%
tulu3
49
33,279
33.35%
Total
211
99,794
Sources: allenai/tulu-3-sft-mixture,
AI-MO/NuminaMath-CoT,
HuggingFaceH4/no_robots.
Example counts differ per source at equal token budgets… See the full description on the dataset page: https://huggingface.co/datasets/dougalldeepmind/2026-08-02-qwen36-mixture-100k-tulu-numina-norobots.2026-08-03-qwen36-mixture-500k-numina-only
Qwen3.6-27B SFT mixture — 500k tokens, NuminaMath-CoT only
497,968 tokens across 934 conversations, drawn entirely from
AI-MO/NuminaMath-CoT. md5 439d58c239e7fc8f23486324a08a7212.
Single-domain by design: no TULU3, No Robots or difficult-advice data. It isolates what maths
chain-of-thought SFT alone does, against the mixed corpora in the sibling datasets.
Format
Every row is a pre-rendered Qwen3.6 chat string with no <think> block -- not even an
empty one, which… See the full description on the dataset page: https://huggingface.co/datasets/dougalldeepmind/2026-08-03-qwen36-mixture-500k-numina-only.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.2026-08-02-qwen36-mixture-500k-da20-numina
Qwen3.6-27B SFT mixture — 500k, 20% difficult-advice + maths-weighted remainder
499,344 tokens across 857 conversations.
md5 416c72ef854a66d0036566c6e9ccec24.
Source
Examples
Tokens
Share
Think block
difficult-advice (synthdoc_v2)
56
95,813
19.19%
real reasoning trace
NuminaMath-CoT
492
269,451
53.96%
none
No Robots
215
67,345
13.49%
empty marker
TULU3
94
66,735
13.36%
empty marker
Total
857
499,344
Within the non-difficult-advice 80.8%: NuminaMath… See the full description on the dataset page: https://huggingface.co/datasets/dougalldeepmind/2026-08-02-qwen36-mixture-500k-da20-numina.NuminaMath-CoT-Small-Hard-200k
Summary
This dataset is a scaled down version of the original AI-MO/NuminaMath-CoT dataset with more focus on hard math.
Source breakdown
Source
Number of Originial Samples
Number of Samples in This Dataset
aops_forum
30201
5000
amc_aime
4072
4070
cn_k12
276591
55310
gsm8k
7345
1000
math
7478
1000
olympiads
150581
37640
orca_math
153334
30662
synthetic_amc
62111
31054
synthetic_math
167895
33574
Total
859608
199310
2026-08-02-qwen36-mixture-500k-numina-heavy
Qwen3.6-27B SFT mixture — 500k tokens, maths-weighted
498,035 tokens across 1,001 conversations, weighted
toward maths: NuminaMath-CoT ~67%, TULU3 and No Robots sharing the remaining ~33%.
md5 5d4d51e3e48c32d103ddf60930b3b0ca.
Source
Examples
Tokens
Share
no_robots
271
82,239
16.51%
numinamath_cot
611
333,351
66.93%
tulu3
119
82,445
16.55%
Total
1001
498,035
Sources: allenai/tulu-3-sft-mixture,
AI-MO/NuminaMath-CoT,
HuggingFaceH4/no_robots.
Example counts… See the full description on the dataset page: https://huggingface.co/datasets/dougalldeepmind/2026-08-02-qwen36-mixture-500k-numina-heavy.NuminaMath-LEAN-satp
NuminaMath-LEAN-satp
Lean 4 formal-statement + initial proof goal_state pairs harvested from
the NuminaMath-LEAN problem pool. This is the main training set for
SATP (Steering Aesop for Theorem Proving) and the target distribution
that all sibling datasets in this collection align with byte-for-byte.
Sibling datasets (same uuid scheme so they join cleanly):
NuminaMath-LEAN-satp-gaps — augmented train set with sub-goal (gap) records harvested from verified sketches… See the full description on the dataset page: https://huggingface.co/datasets/ChristianZ97/NuminaMath-LEAN-satp.AI-MO-NuminaMath-CoT-Ko
Dataset Card for NuminaMath CoT Korean
🎉 Translation finished! If there are any errors, please open the PR. 🎉
If you use this data, please make sure to credit my source!
⚠️ There may be errors in the translation of mathematical terms. (ex: trivial-사소한X/자명한O, negative-부정?음수?)
Translation
The original data AI-MO/NuminaMath-CoT is in English.
I used solar-1-mini-translate-enko-240507 to translate into Korean. To see the detailed script on how I did it, please refer to the… See the full description on the dataset page: https://huggingface.co/datasets/ChuGyouk/AI-MO-NuminaMath-CoT-Ko.NuminaMath-LEAN-cleaned
NuminaMath-LEAN-cleaned
Dataset Description
This is a cleaned and filtered version of AI-MO/NuminaMath-LEAN dataset, optimized for theorem proving training.
Cleaning Process
The dataset has been automatically cleaned with the following improvements:
Removed all comments: Removed /- -/ multi-line and -- single-line commentsRemoved sorry keywords: Cleaned up incomplete proofsStandardized endings: All statements end with := byFiltered declarations: Only kept… See the full description on the dataset page: https://huggingface.co/datasets/ChristianZ97/NuminaMath-LEAN-cleaned.NuminaMath-CoT
Dataset Card for NuminaMath CoT
Dataset Summary
Approximately 860k math problems, where each solution is formatted in a Chain of Thought (CoT) manner. The sources of the dataset range from Chinese high school math exercises to US and international mathematics olympiad competition problems. The data were primarily collected from online exam paper PDFs and mathematics discussion forums. The processing steps include (a) OCR from the original PDFs, (b) segmentation into… See the full description on the dataset page: https://huggingface.co/datasets/skyzos/NuminaMath-CoT.Numina
Numina-Olympiads
Filtered NuminaMath-CoT dataset containing only olympiads problems with valid answers.
Dataset Information
Split: train
Original size: 41012
Filtered size: 38772
Source: olympiads
All examples contain valid boxed answers
Dataset Description
This dataset is a filtered version of the NuminaMath-CoT dataset, containing only problems from olympiad sources that have valid boxed answers. Each example includes:
A mathematical word problem
A… See the full description on the dataset page: https://huggingface.co/datasets/artnoage/Numina.Numina_medium
Numina-Olympiads
Filtered NuminaMath-CoT dataset containing only olympiads problems with valid answers.
Dataset Information
Split: train
Original size: 37133
Filtered size: 37133
Source: olympiads
All examples contain valid boxed answers
Dataset Description
This dataset is a filtered version of the NuminaMath-CoT dataset, containing only problems from olympiad sources that have valid boxed answers. Each example includes:
A mathematical word problem
A… See the full description on the dataset page: https://huggingface.co/datasets/Metaskepsis/Numina_medium.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.mirror-AI-MO__NuminaMath-CoT
Dataset Card for NuminaMath CoT
Dataset Summary
Approximately 860k math problems, where each solution is formatted in a Chain of Thought (CoT) manner. The sources of the dataset range from Chinese high school math exercises to US and international mathematics olympiad competition problems. The data were primarily collected from online exam paper PDFs and mathematics discussion forums. The processing steps include (a) OCR from the original PDFs, (b) segmentation… See the full description on the dataset page: https://huggingface.co/datasets/leeaandrob/mirror-AI-MO__NuminaMath-CoT.NuminaMath-CoT
Dataset Card for NuminaMath CoT
Dataset Summary
Approximately 860k math problems, where each solution is formatted in a Chain of Thought (CoT) manner. The sources of the dataset range from Chinese high school math exercises to US and international mathematics olympiad competition problems. The data were primarily collected from online exam paper PDFs and mathematics discussion forums. The processing steps include (a) OCR from the original PDFs, (b) segmentation into… See the full description on the dataset page: https://huggingface.co/datasets/modibboali/NuminaMath-CoT.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-CoT
Dataset Card for NuminaMath CoT
Dataset Summary
Approximately 860k math problems, where each solution is formatted in a Chain of Thought (CoT) manner. The sources of the dataset range from Chinese high school math exercises to US and international mathematics olympiad competition problems. The data were primarily collected from online exam paper PDFs and mathematics discussion forums. The processing steps include (a) OCR from the original PDFs, (b) segmentation into… See the full description on the dataset page: https://huggingface.co/datasets/woolee0822/NuminaMath-CoT.NuminaMath-CoT
Dataset Card for NuminaMath CoT
Dataset Summary
Approximately 860k math problems, where each solution is formatted in a Chain of Thought (CoT) manner. The sources of the dataset range from Chinese high school math exercises to US and international mathematics olympiad competition problems. The data were primarily collected from online exam paper PDFs and mathematics discussion forums. The processing steps include (a) OCR from the original PDFs, (b) segmentation… See the full description on the dataset page: https://huggingface.co/datasets/chilomax/NuminaMath-CoT.NuminaMath-CoT
Dataset Card for NuminaMath CoT
Dataset Summary
Approximately 860k math problems, where each solution is formatted in a Chain of Thought (CoT) manner. The sources of the dataset range from Chinese high school math exercises to US and international mathematics olympiad competition problems. The data were primarily collected from online exam paper PDFs and mathematics discussion forums. The processing steps include (a) OCR from the original PDFs, (b) segmentation into… See the full description on the dataset page: https://huggingface.co/datasets/primenumbersam/NuminaMath-CoT.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.
