/autoprove

name: autoprove
description: Autonomous multi-cycle theorem proving with explicit stop budgets
user_invocable: true
argument-hint: '[scope] [--max-cycles=N] [--max-total-runtime=DURATION] [--commit=auto|never] [--deep=never|stuck]'

Lean4 Autoprove

Autonomous multi-cycle theorem proving. Runs cycles automatically with explicit stop budgets and structured summaries.

Usage

/lean4:autoprove                        # Start autonomous session
/lean4:autoprove File.lean              # Focus on specific file
/lean4:autoprove --repair-only          # Fix build errors without filling sorries
/lean4:autoprove --max-cycles=10        # Limit total cycles

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. Call `lean4-skills-cycle-tracker init` with resolved numeric values for `--max-cycles`, `--max-stuck-cycles`, `--max-total-runtime`, `--max-deep-per-cycle`, and `--max-consecutive-deep-cycles`. A failed init (exit 2) is a startup validation error — do not proceed. 4. The state file is the single source of truth for session counters. Read counters from `tick`/`status` output, not from conversational memory. 5. With `--persist`: after the tracker is initialized and a valid first dispatch (with its `file_baseline`) exists, 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`; on drift or an uncovered file **stop before any edit and before custody** with an operational-error handoff naming what needs reconciliation (never accept drift automatically); otherwise `run-persist custody`, then `start` with `--reuse-report` ([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 | on | `on` or `off` | | --review-source | No | internal | `internal`, `external`, `both`, or `none` (see coercion below) | | --review-every | No | checkpoint | `N` (sorries), `checkpoint`, or `never` | | --checkpoint | No | true | Create checkpoint commits after each cycle | | --deep | No | stuck | `never`, `stuck`, or `always` (`ask` coerced to `stuck` — see Deep Mode) | | --deep-sorry-budget | No | 2 | Max sorries per deep invocation | | --deep-time-budget | No | 20m | Advisory: scopes deep-mode subagent work. Not tracked or enforced by session tracker. | | --max-deep-per-cycle | No | 1 | Max deep invocations per cycle | | --max-consecutive-deep-cycles | No | 2 | Hard cap on consecutive cycles using deep mode | | --deep-snapshot | No | stash | V1: `stash` only | | --deep-rollback | No | on-regression | `on-regression`, `on-no-improvement`, `always`, or `never` (see coercion below) | | --deep-scope | No | target | `target` or `cross-file` | | --deep-max-files | No | 2 | Max files per deep invocation | | --deep-max-lines | No | 200 | Max added+deleted lines per deep invocation | | --deep-regression-gate | No | strict | `strict` or `off` (see coercion below) | | --batch-size | No | 2 | Sorries to attempt per cycle (advisory) | | --commit | No | auto | `auto` or `never` (`ask` coerced to `auto` — see note below) | | --golf | No | never | `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). | | --max-cycles | No | 20 | Session stop budget: max total cycles | | --max-total-runtime | No | 120m | Best-effort wall-clock session budget | | --max-stuck-cycles | No | 3 | Session stop budget: max consecutive stuck cycles | | --formalize | No | never | `never` \| `restage` \| `