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 with… See the full description on the dataset page:
https://huggingface.co/datasets/Eduardo9991/Nemotron-Math-Proofs-v1.
