Nemotron-Math-Proofs-v1 是由 NVIDIA 于 2025 年发布的一个大规模数学推理与形式化证明数据集，旨在支持大语言模型在结构化数学推理与 Lean 4 形式化定理证明生成方面的训练与研究。

该数据集包含约 58 万条自然语言数学证明题、约 55 万条对应的 Lean 4 定理形式化陈述，以及约 90 万条模型生成的推理轨迹与可编译通过的 Lean 4 证明代码，适用于形式化数学推理模型、长上下文推理系统及验证驱动推理方法的训练与评估。