/disprove

name: disprove
description: Guided counterexample search with certified refutation
user_invocable: true
argument-hint: '<File.lean:LINE | Namespace.theoremName> [--max-cycles=N] [--max-stuck-cycles=N] [--max-runtime=DURATION] [--commit=auto|ask|never] [--knowledge-search-budget=N]'

Lean4 Disprove

Search for a counterexample to a target proposition and, when possible, produce a Lean proof of its negation. Reports `REFUTED` only when Lean certifies the refutation; otherwise `WITNESS_UNCERTIFIED` (a candidate was found but Lean refused to certify it) or `INCONCLUSIVE` (no candidate found within budgets).

`/lean4:disprove` is **always interactive** — disprove is an exploratory search, and the workflow generates three dynamic menus each cycle (Step 0 knowledge search, Step 1 method, Step 2 config) seeded by accumulated evidence and the Target Profile.

Usage

/lean4:disprove Foo.lean:42                       # File + line (sorry/declaration site)
/lean4:disprove MyNs.SubNs.myThm                  # Qualified theorem name
/lean4:disprove Foo.lean:42 --max-cycles=5
/lean4:disprove Foo.lean:42 --commit=never

Prime Directive

Report `REFUTED` **only** when a Lean term of the negation typechecks under `lake env lean` with no `sorry` or `admit` **and** its axiom set is within the allowed whitelist (`propext`, `Classical.choice`, `Quot.sound`; plus `Lean.ofReduceBool` only under an explicit `native_decide` opt-in this cycle). Fast witnesses and informal heuristics are *hypotheses* until Lean certifies them. See [disprove-engine.md § Prime Directive](../skills/lean4/references/disprove-engine.md#prime-directive--epistemological-strictness).

`REFUTED` is licensed by a **checked closed term of type `¬ TARGET`**, not by the artifact's surface form: `T_counterexample` may be a direct `¬ TARGET` theorem **or** a witness theorem whose named per-shape wrapper (also axiom-checked) derives `¬ TARGET`.

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.

**Runtime requirement:** `/lean4:disprove` requires **Python 3.11+** — its method registry loader (`lib/disprove_methods.py`) uses the stdlib `tomllib` parser. The rest of the lean4 plugin targets Python 3.10+. On an older interpreter the command fails fast with a clear "requires Python 3.11+" error rather than an opaque `ImportError`.

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-runtime`, and `--max-knowledge-search-per-cycle=<--knowledge-search-budget>`. Disprove has no deep mode in v1; omit the deep args and let the tracker default them (they remain inert because disprove never calls `can-deep` / `deep`). A failed init (exit 2) is a startup validation error — do not proceed. 4. The cycle-tracker 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 | |-----|----------|---------|-------------| | target | Yes | — | `File.lean:LINE` or `Namespace.theoremName`. Inline Props not supported in v1. A qualified name containing a prime (`'`) or an escaped `«…»` identifier is not accepted in v1 — use a `File.lean:LINE` target for that declaration. | | --max-cycles | No | 3 | Max widening passes. Each cycle picks one method via the Step 1 menu and configures its parameters via the Step 2 menu. | | --max-stuck-cycles | No | 2 | Bail after this many consecutive cycles where the next cycle's Step 1 menu has no non-failed `(family, config)` pair to place in its top 3 (no remaining widening lever). | | --max-runtime | No | 5m | Best-effort wall-clock session budget across all cycles. | | --negation-policy | No | counterexample-only | Reserved for future salvage modes; locked in v1. | | --commit | No | ask | Per-cycle Checkpoint behavior. `ask` prompts before each commit; `auto` commits without prompting; `never` skips committing (leave staging to `/lean4:checkpoint`). | | --knowledge-search-budget | No | 3 | Max Step 0 (knowledge search) visits per cycle. Cycle 1 always runs Step 0 once; later cycles only re-enter Step 0 if their Step 1 menu surfaces `knowledge search` and the user picks it. After the Nth visit completes, `knowledge search` is disabled in that cycle's Step 1 menu. |

Per-method parameters (e.g. enumerate's range, `native_decide` opt-in, sample count for `plausible`) are surfaced as **dynamic Step 2 candidates** in each cycle's Plan phase, not top-level flags. See [disprove-engine.md § Step 2 — Config Menu](../skills/lean4/references/disprove-engine.md#step-2--config-menu).

Actions

Six phases — see [disprove-engine.md](../skills/lean4/references/disprove-engine.md) for full mechanics.

Phase 1: Plan

During Plan, the cycle builds three dynamic menus from accumulated evidence, the Target Profile, and the prior cycle's Review:

• **Step 0 — Knowledge Search** ([engine](../skills/lean4/references/disprove-engine.md#step-0--knowledge-search-menu))
• **Step 1