/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.

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` |

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

See [cycle-engine: LSP-First Protocol](../skills/lean4/references/cycle-engine.md#lsp-first-protocol). Discover sorries via LSP, search with up to 3 tools (~30s), show plan and get confirmation.

Phase 2: Work (Per Sorry)

See [sorry-filling.md](../skills/lean4/references/sorry-filling.md) and [cycle-engine: LSP-First Protocol](../skills/lean4/references/cycle-engine.md#lsp-first-protocol).

1. Refresh goal → search → generate 2-3 candidates → test via `lean_multi_attempt` 2. Preflight falsification for decidable/finite goals (30-60s max) 3. Tactic cascade if no candidate passed 4. Validate via `lean_diagnostic_messages`; if "Try this" suggestion appears, resolve with `lean_code_actions`, then re-run `lean_diagnostic_messages` to confirm clean 5. Stage & commit (see below)

**Staging rule:** If `--commit=never`, skip staging and committing entirely. Otherwise, stage only the files touched by this fill (`git add <edited files>`) — never `git add -A` or broad patterns.

**Touched-file reporting:** At session end, report `files_touched` (files edited) and `scratch_files_created` (any `/tmp` files used for experiments).

**Commit behavior** (unique to prove): Show diff and ask before each commit when `--commit=ask` (default):

Commit this? [yes / yes-all / no / never]

• **yes** — commit, prompt again next time
• **yes-all** — switch to `auto` for rest of session
• **no** — unstage (`git reset HEAD <files>`), skip this commit
• **never** — unstage, skip all remaining commits for session

**Constraints:** Max 3 candidates per sorry, ≤80 lines diff, NO statement changes, NO cross-file refactoring (fast path). Declaration headers are immutable — if deep mode suggests a header change, it must stop and recommend `/lean4:formalize`.

Phase 3: Checkpoint

See [cycle-engine: Checkpoint Logic](../skills/lean4/references/cycle-engine.md#checkpoint-logic). Stage only files from **accepted** fills;