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.
Conversations for this repository live on Hugging Face.
CoolFace shows imported repositories read-only. Posting into someone else’s repository from here would need an authorised integration and the account holder’s consent, so the link goes to the source instead.
Open discussions on Hugging Face