NuminaMath-LEAN est un ensemble de données de problèmes mathématiques publié conjointement par Numina et Kimi Team en 2025. Les résultats de l'article associé sont «Aperçu de Kimina-Prover : Vers de grands modèles de raisonnement formel avec apprentissage par renforcement", qui vise à fournir des énoncés formels et des preuves annotés manuellement pour la formation et l'évaluation de modèles automatisés de démonstration de théorèmes.

Cet ensemble de données contient 100 000 problèmes de compétitions mathématiques, dont ceux issus de compétitions de référence telles que l'Olympiade internationale de mathématiques (IMO) et l'Olympiade américaine de mathématiques (USAMO). Les types de données incluent les énoncés de problèmes, les classifications des types de questions, les réponses, les sources, les preuves formelles, les informations des annotateurs et les enregistrements des processus d'apprentissage par renforcement.