NuminaMath-LEAN هي مجموعة بيانات لمشكلات رياضية تم إصدارها بشكل مشترك من قبل Numina وفريق Kimi في عام 2025. نتائج الورقة ذات الصلة هي "معاينة كيمينا-بروفر: نحو نماذج استدلال شكلية كبيرة مع التعلم التعزيزي"، والذي يهدف إلى توفير عبارات رسمية موضحة يدويًا وإثباتات لتدريب وتقييم نماذج إثبات النظرية الآلية.

تحتوي هذه المجموعة من البيانات على 100,000 مسألة رياضية، بما في ذلك مسائل من مسابقات معتمدة مثل أولمبياد الرياضيات الدولي (IMO) وأولمبياد الرياضيات الأمريكي (USAMO). تتضمن أنواع البيانات عبارات المسائل، وتصنيفات أنواع الأسئلة، والإجابات، والمصادر، والبراهين الرسمية، ومعلومات المُعلّق، وسجلات عملية تدريب التعلم المُعزّز.