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

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` | | --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` \| `auto`. See Formalize Outer Loop. (deprecated: use `/lean4:autoformalize`) | | --source | No | — | File path, URL, or PDF for claim extraction. Required when `--formalize=auto`. (deprecated: use `/lean4:autoformalize`) | | --claim-select | No | — | `first` \| `named:"..."` \| `regex:"..."`. Queue-extraction filter applied once at startup. Required when `--formalize=auto`. Ignored without `--source`. (deprecated: use `/lean4:autoformalize`) | | --formalize-rigor | No | sketch | `sketch` \| `checked`. Rigor for formalize skeleton. (deprecated: use `/lean4:autoformalize --rigor`) | | --statement-policy | No | preserve | `preserve` \| `rewrite-generated-only` \| `adjacent-drafts`. Default becomes `rewrite-generated-only` when `--formalize=restage\|auto` (see flag validation). (deprecated: use `/lean4:autoformalize`) | | --formalize-out | No | — | Target file for formalized claims. Required if no existing target in scope. (deprecated: use `/lean4:autoformalize --out`) |

Review Source Coercion

Autoprove accepts all `--review-source` values for flag compatibility with `/lean4:prove`. However, autoprove **never blocks waiting for interactive input**. If the value is `external` or `both`, autoprove coerces to `internal` at startup and emits:

> ⚠ --review-source=external requires interactive handoff. Using internal review for unattended operation.

> **Future autonomous external review:** External review is currently manual-handoff only. Future versions may support autonomous external review via non-interactive CLI execution (e.g., `codex exec`) behind an explicit opt-in flag (`--external-autonomous`). Until then, unattended autoprove runs default to internal review. > > Requirements for autonomous external review: > 1. Stable JSON input/output contract > 2. Timeout + retry + cost budgets > 3. Safe fallback to internal review on external failure > 4. Explicit opt-in flag, not default behavior

Formalize Flag Validation

• `--formalize=auto`