{"data":{"kind":"file","path":"README.md","version_id":"yna6kdjv35x54ma7jmj3cb3n","entry":{"name":"README.md","path":"README.md","is_directory":false,"size":1177,"modified_at":"2026-09-13T04:06:06.924000","content_hash":"62b48427ad4df98b3b1996106c8454065204f38b3458cab7970a5521e29e2e4e"},"entries":[],"content":"# deepseek-prover\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-Prover-V1`](https://huggingface.co/datasets/deepseek-ai/DeepSeek-Prover-V1) — 27503 tasks (train)\n\n## Changelog\n\n- 2026-09-03: Restore default solver network access by reverting the `network_allow=[]` default-deny policy introduced in #780; training rollouts need outbound network.\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":1177},"status":null}