{"data":{"kind":"file","path":"README.md","version_id":"piaw4u6a95gwy5sfkccjnhrw","entry":{"name":"README.md","path":"README.md","is_directory":false,"size":1151,"modified_at":"2026-09-13T04:06:06.926000","content_hash":"5a1b43d4a07d68e0e829dd3229563abd4bb8382cdcded7604f5fbd84b9186328"},"entries":[],"content":"# numina\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- [`AI-MO/NuminaMath-LEAN`](https://huggingface.co/datasets/AI-MO/NuminaMath-LEAN) — 104155 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":1151},"status":null}