Nemotron-Math-Proofs-v1 ist ein umfangreicher Datensatz für mathematisches Schließen und formale Beweise, der von NVIDIA im Jahr 2025 veröffentlicht wurde und die Entwicklung und Forschung großer Sprachmodelle im Bereich des strukturierten mathematischen Schließens und der Generierung formaler Theorembeweise mit Lean 4 unterstützen soll.

Dieser Datensatz enthält ca. 580.000 mathematische Beweisfragen in natürlicher Sprache, ca. 550.000 zugehörige formale Aussagen von Lean-4-Theoremen sowie ca. 900.000 modellgenerierte Inferenztrajektorien und kompilierbaren Lean-4-Beweiscode. Er eignet sich zum Trainieren und Evaluieren formaler mathematischer Schlussfolgerungsmodelle, Systeme für kontextbezogenes Schließen und verifikationsgetriebene Schlussfolgerungsmethoden.