0

Proverbench

Fresh

Lean 4 agentic theorem proving on deepseek-ai/DeepSeek-ProverBench, eval-only (wrapper over the shared verifiers.v1.tasksets.lean base).

Type
RL Env
Publisher
Prime Intellect
Tags
V1AgenticTheorem ProvingLean4Mathlib
Runtime
agent
License
unknown
Size
v0.1.0
Published
Aug 2026
Updated
Sep 2026
Canonical
app.primeintellect.ai/dashboard/environments/primeintellect/proverbench

Cite

Notes

Only stored in your browser.

Attribution

Attribution policy →

proverbench

Lean 4 agentic theorem proving: a thin per-dataset wrapper over the shared verifiers.v1.tasksets.lean base, which plants a sorry starter proof in a Mathlib sandbox and rewards a clean lake env lean compile (with a guard pinning the theorem statement). Needs a container runtime.

Taskset

Notes

  • Held-out eval-only benchmark — do not train on it (leakage).

Changelog

  • 2026-08-31: Yield task records on demand so bounded evaluations construct only the requested prefix.
  • 2026-07-29: Split out of the lean_v1 bundle into its own environment (one dir per taskset, environments/lean/ group).
  • 2026-07-10: Ported to the task-centric verifiers API: rewards and lifecycle hooks live on the Task (a TaskData row + behavior split), and task-facing config knobs (judges, tool/user placement, scoring parameters) moved from --env.taskset.* to --env.taskset.task.*. Requires verifiers>=0.2.0 and Python >=3.11.