Nemotron-Math-Proofs

Description

Nemotron-Math-Proofs is a Lean 4 formal proof verification environment built on NVIDIA's Nemotron-Math-Proofs-v1 dataset. Agents receive a mathematical theorem as a Lean 4 formal statement and must produce a valid proof that compiles successfully with the Lean 4 toolchain and Mathlib4.

Capabilities

• Generating formal Lean 4 proofs for competition-level mathematics
• Reasoning about algebra, number theory, geometry, topology, and analysis
• Working with the Mathlib4 library of formalized mathematics
• Translating mathematical reasoning into machine-verified proofs

Compute Requirements

Proof verification runs in a sandbox with 1 CPU and 2GB RAM, using a custom Docker image (generalreasoning/lean4-mathlib:v4.12.0) with Lean 4 and pre-built Mathlib4 cache.

License

CC BY-SA 4.0 (matching the original dataset license).

Tasks

Single train split containing unique theorems extracted from Nemotron-Math-Proofs-v1. Each theorem includes:

• Natural language problem statement
• Lean 4 formal theorem declaration
• Mathlib4 import header

Difficulty levels (based on pass@4 initial success rate):

• hard: 1/4 initial proofs succeeded
• medium: 2/4 initial proofs succeeded
• easy: 3/4 initial proofs succeeded
• very_easy: 4/4 initial proofs succeeded

Reward Structure

Binary, verifiable reward with no LLM graders:

• 1.0: Proof compiles successfully with Lean 4 + Mathlib4, no sorry tactic
• 0.0: Compilation failure, timeout (30s), or sorry usage

Data

Theorems sourced from Nemotron-Math-Proofs-v1, which contains problems from Art of Problem Solving (AoPS) and Math StackExchange, autoformalized into Lean 4 with verified proofs.

Tools

• answer: Submit a Lean 4 proof for verification. The proof is compiled with the Lean 4 toolchain in a sandboxed environment. Returns compilation result and reward.

Time Horizon

Single-turn: the agent receives the theorem and submits one proof attempt.

Other Environment Requirements

No other requirements.

Safety

Agents interact only with a formal proof verification system. Code execution is sandboxed and restricted to Lean 4 compilation. There are no external API calls, network access requirements, or real-world side effects.

Citations

@dataset{NemotronMathProofsV1,
  author    = {NVIDIA},
  title     = {Nemotron-Math-Proofs-v1},
  year      = {2026},
  publisher = {Hugging Face},
  url       = {https://huggingface.co/datasets/nvidia/Nemotron-Math-Proofs-v1},
  license   = {CC BY-SA 4.0}
}