Datasetpublic

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.

sourceHugging Facecc-by-sa-4.0updated 9mo agoView on Hugging Face

0likes26downloads

settings

This repository belongs to Eduardo9991 on Hugging Face.

CoolFace never edits a repository it does not host. Visibility, licence, collaborators and gating are all managed at the source.

nameNemotron-Math-Proofs-v1

visibilitypublic

licencecc-by-sa-4.0

gatedno

ownerEduardo9991

Account settings