{"data":{"kind":"file","path":"README.md","version_id":"lanpfh1bf800ysb6xidrg42f","entry":{"name":"README.md","path":"README.md","is_directory":false,"size":1076,"modified_at":"2026-09-16T12:25:28.042000","content_hash":"6e39df6bb7ec49b6a7bece523cfb8316803759b5032d669c4cc64a81d84935eb"},"entries":[],"content":"# minif2f\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- [`cat-searcher/minif2f-lean4`](https://huggingface.co/datasets/cat-searcher/minif2f-lean4) — 244 tasks (test, 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":1076},"status":null}