Nemotron-Math-Proofs-v1 は、NVIDIA が 2025 年にリリースした大規模な数学的推論および形式的証明データセットであり、構造化された数学的推論と Lean 4 形式定理証明生成における大規模言語モデルのトレーニングと研究をサポートするように設計されています。

このデータセットには、約58万件の自然言語による数学証明問題、約55万件の対応するLean 4定理の形式的記述、約90万件のモデル生成推論軌跡、およびコンパイル可能なLean 4証明コードが含まれています。形式数学推論モデル、長文脈推論システム、検証駆動型推論手法の訓練と評価に適しています。