Nemotron-Math-Proofs-v1 est un ensemble de données de raisonnement mathématique et de preuves formelles à grande échelle publié par NVIDIA en 2025, conçu pour soutenir l'entraînement et la recherche de grands modèles de langage dans le raisonnement mathématique structuré et la génération de preuves de théorèmes formels Lean 4.

Cet ensemble de données contient environ 580 000 questions de démonstration mathématique en langage naturel, environ 550 000 énoncés formels correspondants de théorèmes Lean 4, et environ 900 000 trajectoires d'inférence générées par le modèle ainsi que du code de démonstration Lean 4 compilable. Il convient à l'entraînement et à l'évaluation de modèles de raisonnement mathématique formel, de systèmes de raisonnement à contexte long et de méthodes de raisonnement pilotées par la vérification.