Theorem Proving · AI-MO
Kimina-Prover-Promptset
A curated dataset of challenging mathematical problems in Lean 4 for reinforcement learning theorem proving.
What Kimina-Prover-Promptset is
Kimina-Prover-Promptset is a mathematical prompt dataset created by AI-MO to train and evaluate automated theorem provers using the Lean 4 interactive proof assistant. The dataset focuses on formal mathematical reasoning and serves as an input corpus for reinforcement learning pipelines.
Formed as a selective subset of NuminaMath-LEAN, the dataset addresses the need for higher problem difficulty when training formal reasoning models. By discarding easier problems and emphasizing more complex mathematical challenges, it provides training material structured to improve proof-search performance.
How it was made
The dataset is derived from NuminaMath-LEAN through filtering, augmentation, and re-weighting. Tasks with a historical win rate above 0.5 are eliminated so that only difficult statements remain. Gemini is used to generate variations of existing statements to expand mathematical diversity, and particularly hard problems are duplicated to accord them greater weight during reinforcement learning.
The corpus is stored in Parquet format. Each entry contains a unique statement identifier, the problem formulated in natural language, the corresponding formal statement written in Lean 4, the problem name, and an indicator marking whether the record is original or synthetic.
Key facts
- Format
- Parquet
- Modality
- Text
- Target language
- Lean 4
- Base dataset
- NuminaMath-LEAN
What you can use it for
- Reinforcement Learning for Formal Proofs
- Supplying prompts and formal environments for reinforcement learning runs that train models to generate Lean 4 proofs, as demonstrated with Kimina-Prover-RL-1.7B.
- Theorem Prover Evaluation
- Benchmarking and evaluating the mathematical capabilities and formal verification success rates of automated theorem provers.
- Synthetic Mathematical Data Research
- Investigating how LLM-generated problem variants and duplicated challenging prompts affect formal reasoning performance.
Explore the data
No licence declared
The authors have not published a licence, which means no permission to redistribute the data has been granted to anyone. The rows are not served here; read them on the original dataset page.How the columns are distributed
Over 24,418 rows of default/train
formal_statement
string_text- min
- 74
- median
- 332
- mean
- 371.98
- max
- 4,382
name
string_text- min
- 3
- median
- 20
- mean
- 19.15
- max
- 42
natural_language
string_text- min
- 26
- median
- 163
- mean
- 192.00
- max
- 2,349
0.05% empty
source
string_label- synthetic41%
- autoformalizer32%
- human27%
statement_id
string_text- min
- 36
- median
- 36
- mean
- 36
- max
- 36
Strengths and limits
Good at
- Filters out simple problems with historical win rates over 0.5 to concentrate exclusively on difficult statements.
- Augments prompt diversity by including synthetic variants generated by Gemini.
- Applies sample duplication to hard problems to weight them more heavily in model training.
- Paired with proven downstream performance, having trained a 1.7B model that achieved 76.63% Pass@32 on MiniF2F.
Watch out for
- Contains only statements formulated for the Lean 4 proof environment.
- Omits introductory and easier problems, making it unsuitable for baseline calibrations that require broad difficulty ranges.
- Contains synthetically generated statements that may introduce generative model artifacts.
Questions
Can I look inside Kimina-Prover-Promptset without downloading it?
Not here: it declares no licence, so no permission to redistribute its rows has been granted. Its description and statistics are still shown.
What licence is Kimina-Prover-Promptset under?
Its authors have not declared a licence, which means no permission to reuse or redistribute it has been granted.
What is the relationship between this dataset and NuminaMath-LEAN?
Kimina-Prover-Promptset is a curated subset of NuminaMath-LEAN that keeps harder problems, removes problems with a historical win rate above 0.5, and adds synthetic variants.
Which models have been trained with this dataset?
It was used to train AI-MO/Kimina-Prover-RL-1.7B, a 1.7-billion-parameter Lean 4 prover that achieved a 76.63% Pass@32 score on the MiniF2F benchmark.
What columns are included in the dataset?
The dataset contains statement_id, natural_language, formal_statement, source (marked as 'synthetic' when generated), and name.
How to cite it
Wang, H., Unsal, M., Lin, X., Baksys, M., Liu, J., Santos, M. D., Sung, F., Vinyes, M., Ying, Z., Zhu, Z., Lu, J., Saxce, H. d., Bailey, B., Song, C., Xiao, C., Zhang, D., Zhang, E., Pu, F., Zhu, H., Liu, J., Bayer, J., Michel, J., Yu, L., Dreyfus-Schmidt, L., Tunstall, L., Pagani, L., Machado, M., Bourigault, P., Wang, R., Polu, S., Barroyer, T., Li, W.-D., Niu, Y., Fleureau, Y., Hu, Y., Yu, Z., Wang, Z., Yang, Z., Liu, Z., & Li, J. (2025). Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning. arXiv:2504.11354.
Written from Kimina-Prover-Promptset's own dataset card. Statements citing a figure that does not appear there are removed before publication. Licence and running details come from our registry.