NuminaMath-LEAN 是由 Numina 和 Kimi Team 于 2025 年联合发布的一个数学问题数据集，相关论文成果为「Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning」，旨在为自动化定理证明模型的训练与评估提供人工标注的形式化陈述与证明。 该数据集包含 10 万个数学竞赛问题，问题涵盖国际数学奥林匹克（IMO）、美国数学奥林匹克（USAMO）等权威赛事题目，数据类型包括问题陈述、题型分类、答案、来源、形式化证明、标注者信息及强化学习训练过程记录。

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}, }