Nemotron-Math-Proofs-v1은 NVIDIA에서 2025년에 공개한 대규모 수학적 추론 및 형식 증명 데이터셋으로, 구조화된 수학적 추론 및 Lean 4 형식 정리 증명 생성 분야에서 대규모 언어 모델의 학습 및 연구를 지원하도록 설계되었습니다. 이 데이터셋은 약 58만 개의 자연어 수학적 증명 문제, 약 55만 개의 Lean 4 정리의 형식적 명제, 그리고 약 90만 개의 모델 생성 추론 궤적 및 컴파일 가능한 Lean 4 증명 코드로 구성되어 있습니다. 형식적 수학적 추론 모델, 장기 문맥 추론 시스템, 그리고 검증 기반 추론 방법의 학습 및 평가에 적합합니다.