NuminaMath-LEAN ist ein mathematischer Problemdatensatz, der 2025 gemeinsam von Numina und dem Kimi-Team veröffentlicht wurde. Die zugehörigen Papierergebnisse sind „Kimina-Prover-Vorschau: Auf dem Weg zu großen formalen Argumentationsmodellen mit bestärkendem Lernen“, dessen Ziel darin besteht, manuell annotierte formale Aussagen und Beweise für das Training und die Evaluierung automatisierter Theorembeweismodelle bereitzustellen.

Dieser Datensatz enthält 100.000 Mathematikwettbewerbsaufgaben, darunter auch Aufgaben aus renommierten Wettbewerben wie der Internationalen Mathematik-Olympiade (IMO) und der US-amerikanischen Mathematik-Olympiade (USAMO). Die Datentypen umfassen Problemstellungen, Fragetypklassifizierungen, Antworten, Quellen, formale Beweise, Anmerkungsinformationen und Aufzeichnungen des Trainingsprozesses für bestärkendes Lernen.