Add KiminaProver (whole-proof generation prover)

[henryrobbins]

Adds Moonshot AI's Kimina-Prover as a registered prover (kimina): a whole-proof generation model we serve ourselves on GPU via vLLM. Structurally the Aristotle path (generate → splice → verify), with generation isolated behind a _generate seam so the splice/select/guard logic is fully testable offline.

Phase A — adapter (generation stubbed)

• provers/_lean_splice.py — provider-agnostic, offset-preserving extract_theorems / splice_proof helpers (shared with the deferred BFS path). Bracket-aware so a := inside a signature isn't mistaken for the proof delimiter.
• provers/kimina.py — KiminaProver + KiminaProverConfig. prove(): stage → extract sorry'd targets → _generate (test seam) → select by authoritative compile (first candidate that compiles, is sorry-free, and passes the StatementTracker signature guard wins) → diff. cost_usd=None; pass_k / samples_tried / per-target winning_index in metadata.
• api.py — kimina registry entry; the platform's agent backend doubles as Kimina's generation backend. No toolchain-gate change.
• backends/modal.py — ModalConfig.gpu, passed to Sandbox.create.

Phase B — GPU image + generation entrypoint

• images/kimina/kimina_generate.py — one-shot vLLM entrypoint. Prompt format + sampling pinned to the model card recipe (temperature=0.6 top_p=0.95, n=pass_k). Extracts the proof body (tactic block after by) from the last complete fenced Lean block. vLLM/transformers imports deferred so helpers unit-test with no GPU.
• images/kimina.Dockerfile — based on the official vLLM image, layering the standard Lean toolchain + warm Mathlib cache. Weights downloaded to a mounted Volume.
• backends/modal.py — ModalConfig.volumes → named Modal Volumes (persist weights / HF cache).
• __main__.py — build-kimina-image CLI (publishes a Modal image named kimina).

Phase C — partial (offline-testable wins)

• Informal-problem context: extract_theorems captures each declaration's preceding doc comment (Theorem.docstring); threaded into generation as the problem field (per-target docstring, else task instructions).
• Model-size knob: kimina:7b / kimina:1.5b registry variants; bare kimina keeps the 7B default.

Tests

tests/test_kimina_prover.py — pure helper coverage (incl. docstring extraction), pass@k selection + guard with a fake verifier, build_prompt/extract_proof_body units, problem-context threading, model-size variants, a Docker-marked end-to-end over the real shared verifier, and a slow Modal-gated real-GPU end-to-end. 54 offline tests pass; ruff + mypy clean.

Remaining (needs a real GPU / infra to build + verify)

• Persistent vLLM server (avoid per-task model load).
• Kimina Lean Server for fast in-sandbox pass@k pre-filtering before the authoritative compile.
• GPU smoke test to close two open model-card questions: confirm the rendered chat template, and the distill's Mathlib revision vs our v4.28.0 pin.

🤖 Generated with Claude Code