NuminaMath-LEAN 数学问题数据集

NuminaMath-LEAN 是由 Numina 和 Kimi Team 于 2025 年联合发布的一个数学问题数据集，相关论文成果为「Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning」，旨在为自动化定理证明模型的训练与评估提供人工标注的形式化陈述与证明。

该数据集包含 10 万个数学竞赛问题，问题涵盖国际数学奥林匹克（IMO）、美国数学奥林匹克（USAMO）等权威赛事题目，数据类型包括问题陈述、题型分类、答案、来源、形式化证明、标注者信息及强化学习训练过程记录。