{"data":{"kind":"file","path":"README.md","version_id":"rr442vnmbuwpj3izj1grclom","entry":{"name":"README.md","path":"README.md","is_directory":false,"size":1086,"modified_at":"2026-09-13T04:06:06.926000","content_hash":"6e6efe388cf596343f1df44582e3ef7210ad62abda09c9fc88268ec6ffe82205"},"entries":[],"content":"# proverbench\n\nLean 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.\n\n## Taskset\n\n- [`deepseek-ai/DeepSeek-ProverBench`](https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench) — 325 tasks (eval-only)\n\n## Notes\n\n- Held-out eval-only benchmark — do not train on it (leakage).\n\n## Changelog\n\n- 2026-08-31: Yield task records on demand so bounded evaluations construct only the requested prefix.\n- 2026-07-29: Split out of the `lean_v1` bundle into its own environment (one dir per taskset, `environments/lean/` group).\n- 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`.\n","encoding":"utf-8","truncated":false,"total_bytes":1086},"status":null}