Eduardo9991/Nemotron-Math-Proofs-v1

Dataset Description: Nemotron-Math-Proofs-v1 is a large-scale mathematical reasoning dataset containing ~580k natural language proof problems, ~550k formalizations into theorem statements in Lean 4, and ~900k model-generated reasoning trajectories culminating in Lean 4 proofs. The dataset integrates human-authored problems with systematically generated formalizations and solution traces. Each natural language problem is formalized by gpt-oss-120b into Lean 4 theorem statements… See the full description on the dataset page: https://huggingface.co/datasets/Eduardo9991/Nemotron-Math-Proofs-v1.