Nemotron-Math-Proofs-v1 is a large-scale mathematical reasoning and formal proof dataset released by NVIDIA in 2025, designed to support the training and research of large language models in structured mathematical reasoning and Lean 4 formal theorem proof generation.

This dataset contains approximately 580,000 natural language mathematical proof questions, approximately 550,000 corresponding formal statements of Lean 4 theorems, and approximately 900,000 model-generated inference trajectories and compileable Lean 4 proof code. It is suitable for training and evaluating formal mathematical reasoning models, long-context reasoning systems, and verification-driven reasoning methods.