autoprove

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.

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.

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)