NuminaMath-LEAN is a mathematical problem dataset jointly released by Numina and Kimi Team in 2025. The related paper results are "Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning", which aims to provide manually annotated formal statements and proofs for the training and evaluation of automated theorem proving models. This dataset contains 100,000 math competition problems, including those from authoritative competitions such as the International Mathematical Olympiad (IMO) and the United States Mathematical Olympiad (USAMO). The data types include problem statements, question type classifications, answers, sources, formal proofs, annotator information, and reinforcement learning training process records.

Citation

@article{kimina_prover_2025, title = {Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning}, author = {Wang, Haiming and Unsal, Mert and Lin, Xiaohan and Baksys, Mantas and Liu, Junqi and Santos, Marco Dos and Sung, Flood and Vinyes, Marina and Ying, Zhenzhe and Zhu, Zekai and Lu, Jianqiao and Saxcé, Hugues de and Bailey, Bolton and Song, Chendong and Xiao, Chenjun and Zhang, Dehao and Zhang, Ebony and Pu, Frederick and Zhu, Han and Liu, Jiawei and Bayer, Jonas and Michel, Julien and Yu, Longhui and Dreyfus-Schmidt, Léo and Tunstall, Lewis and Pagani, Luigi and Machado, Moreira and Bourigault, Pauline and Wang, Ran and Polu, Stanislas and Barroyer, Thibaut and Li, Wen-Ding and Niu, Yazhe and Fleureau, Yann and Hu, Yangyang and Yu, Zhouliang and Wang, Zihan and Yang, Zhilin and Liu, Zhengying and Li, Jia}, year = {2025}, url = {http://arxiv.org/abs/2504.11354}, }