AI-MO

NuminaMath-LEAN

Mathematical problems formalized in LEAN proof assistant.

Rows: 104,155
On disk: 75 MB
Downloads: 1.2k
Updated: Jul 31

Explore

Read the real rows without downloading anything

Reading rows…

LiveRead from AI-MO/NuminaMath-LEAN at the moment you asked. Nothing is cached or stored — every row above came from that request.

Column statistics

How the columns are distributed

Over 104,155 rows of default/train

answer

string_text

min: 0
median: 7
mean: 9.97
max: 231

6.4% empty

author

string_label

autoformalizer81%
human19%

unknown97%
HMMT1%
IMO1%

formal_ground_truth

string_text

min: 0
median: 0
mean: 412.03
max: 69,614

formal_proof

string_text

min: 0
median: 686
mean: 1016.80
max: 14,324

63.0% empty

formal_statement

string_text

min: 60
median: 382
mean: 424.03
max: 29,051

ground_truth_type

string_label

complete9%
statement8%
with_sorry2%

80.7% empty

problem

string_text

min: 14
median: 190
mean: 226.35
max: 9,959

problem_type

string_label

Algebra38%
Number Theory27%
Inequalities14%

question_type

string_label

math-word-problem55%
proof31%
MCQ8%

0.00% empty

source

string_label

olympiads49%
unknown14%
aops_forum12%

uuid

string_text

min: 36
median: 36
mean: 36
max: 36

NuminaMath-LEAN

How the columns are distributed

answer

author

exam

formal_ground_truth

formal_proof

formal_statement

ground_truth_type

problem

problem_type

question_type

source

uuid