/prove

name: prove
description: Guided cycle-by-cycle theorem proving with explicit checkpoints
user_invocable: true
argument-hint: '[scope] [--planning=ask|on|off] [--deep=never|stuck|ask] [--commit=ask|auto|never]'

Lean4 Prove

Guided, cycle-by-cycle theorem proving. Asks before each cycle, supports deep escalation, and checkpoints your progress.

Usage

/lean4:prove                         # Start guided session
/lean4:prove File.lean               # Focus on specific file
/lean4:prove --repair-only           # Fix build errors without filling sorries
/lean4:prove --deep=stuck            # Enable deep escalation when stuck

Invocation Contract

Interpret this command's inputs per the [Command Invocation Contract](../skills/lean4/references/command-invocation.md).

**Primary path (hook-validated):** If a `validated-invocation` block for this command appears in context, treat it as the authoritative interpretation of parser-decidable inputs and do **not** re-parse the raw invocation text for those inputs. Start by reading all parser-decided fields from the block. Emit the final **Resolved Inputs** summary from the block values. See [Validated Invocation Block](../skills/lean4/references/command-invocation.md#validated-invocation-block-host-provided).

**Fallback path (other hosts):** If no `validated-invocation` block is present, parse the raw invocation text against this command's input table before Phase 1.

Startup requirements:

1. Emit a **Resolved Inputs** block with explicit values, defaults, coercions, ignored flags, and startup validation errors. 2. Refuse to start on startup validation errors. 3. Persist any user-approved adjustments as session state so later cycles follow the updated configuration rather than the initial prose alone. 4. With `--persist`: after the checks above and a valid first dispatch, set `LEAN4_RUN_PERSIST_STATE` to a fresh invocation-private path (`mktemp -d` + a not-yet-existing file) and run `lean4-skills-run-persist start` **before any proof edit**; a `startup-error` is a startup validation error. Report the `run_id` in Resolved Inputs and follow [Run Persistence](../skills/lean4/references/cycle-engine.md#run-persistence) at every review, cycle boundary, and stop; for each inline edit: `check` → edit → `advance` (changed entries only) → `run-persist progress --payload` (parent knowledge, no citation; fallbacks reflect reported knowledge only). With `--prior-run`, first run `run-persist reuse`, show the drift report (drift and uncovered files), obtain approval of **that report** (its token), `run-persist custody`, and pass `--reuse-report` (and, when the report was not a match, `--approve <token>`) to `start`, which re-derives custody ([Prior-Run Reuse](../skills/lean4/references/cycle-engine.md#prior-run-reuse)).

Inputs

| Arg | Required | Default | Description | |-----|----------|---------|-------------| | scope | No | all | Specific file or theorem to focus on | | --repair-only | No | false | Fix build errors only, skip sorry-filling | | --planning | No | ask | `ask` (prompt at startup), `on`, or `off` | | --review-source | No | internal | `internal`, `external`, `both`, or `none` | | --review-every | No | checkpoint | `N` (sorries), `checkpoint`, or `never` | | --checkpoint | No | true | Create checkpoint commits after each cycle | | --deep | No | never | `never`, `ask`, `stuck`, or `always` | | --deep-sorry-budget | No | 1 | Max sorries per deep invocation | | --deep-time-budget | No | 10m | Advisory: scopes deep-mode subagent work. Not tracked or enforced. | | --max-deep-per-cycle | No | 1 | Max deep invocations per cycle | | --deep-snapshot | No | stash | V1: `stash` only | | --deep-rollback | No | on-regression | `on-regression`, `on-no-improvement`, `always`, or `never` | | --deep-scope | No | target | `target` or `cross-file` | | --deep-max-files | No | 1 | Max files per deep invocation | | --deep-max-lines | No | 120 | Max added+deleted lines per deep invocation | | --deep-regression-gate | No | strict | `strict` (auto-abort on regression) or `off` | | --batch-size | No | 1 | Sorries to attempt per cycle | | --commit | No | ask | `ask` (prompt before each commit), `auto`, or `never` | | --golf | No | prompt | `prompt`, `auto`, or `never` | | --persist | No | false | Write this run to the run store (dispatches, handoffs, notes, reviews, Replan summaries; one run per invocation). Off by default — existing invocations are unchanged. Platform support is a startup capability check. See [cycle-engine: Run Persistence](../skills/lean4/references/cycle-engine.md#run-persistence). | | --run-store | No | — | Storage root override; requires `--persist` (`--run-store` without `--persist` → startup validation error). Precedence: `--run-store` → `$LEAN4_RUN_STORE` → `<project-root>/.lean4-skills`. | | --prior-run | No | — | Reuse a selected prior run's history (explicit id; never "latest"; resolved within the selected store); requires `--persist` (`--prior-run` without `--persist` → startup validation error). See [cycle-engine: Prior-Run Reuse](../skills/lean4/references/cycle-engine.md#prior-run-reuse). |

Startup Behavior

If key preferences are not passed via flags, ask once at startup:

**Planning preference:** > Start with a planning phase? (Recommended for new sessions) > 1) Yes — discover state, set scope, show plan (recommended) > 2) No — skip planning, start immediately

**Review source:** > How should reviews be conducted? > 1) Internal — planner mode reviews and can apply fixes (recommended) > 2) External — interactive handoff for advice only > 3) Both — internal first, then external advice > 4) None — no automatic reviews

If `--planning=off`, skip initial planning but stuck-triggered replan is still mandatory (see Stuck Definition).

Actions

Each cycle has 6 phases — see [cycle-engine.md](../skills/lean4/references/cycle-engine.md) for shared mechanics.

Phase 1: Plan