0

Kimina

Fresh

Lean 4 agentic theorem proving on AI-MO/Kimina-Prover-Promptset (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.1
Published
Aug 2026
Updated
Sep 2026
Canonical
app.primeintellect.ai/dashboard/environments/primeintellect/kimina

Cite

Notes

Only stored in your browser.

Attribution

Attribution policy →

kimina

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

Changelog

  • 2026-09-03: Restore default solver network access by reverting the network_allow=[] default-deny policy introduced in #780; training rollouts need outbound network.
  • 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.