/review

name: review
description: Read-only code review of Lean proofs
user_invocable: true

Lean4 Review

Read-only review of Lean proofs for quality, style, and optimization opportunities.

**Non-destructive:** Files are restored after analysis.

Usage

/lean4:review                              # Review changed files (default)
/lean4:review File.lean                    # Review specific file
/lean4:review File.lean --line=89          # Review single sorry
/lean4:review File.lean --line=89 --scope=deps  # Review sorry + its dependencies
/lean4:review --scope=project              # Review entire project (prompts)
/lean4:review --mathlib-review             # Force the mathlib-review bar (Layer 2)

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

Startup requirements:

1. Emit a **Resolved Inputs** block with explicit values, defaults, and any ignored flags — including the effective **Layer-2 activation** decision and its source (`flag`, `repository_kind`, `contributing_upstream`, the helper's validated `intent.source`, or `helper-failure`; see [Mathlib Review Layer](#mathlib-review-layer-layer-2)). 2. Refuse to start on startup validation errors — including passing both `--mathlib-review` and `--no-mathlib-review` (`--mathlib-review` with `--no-mathlib-review` → startup validation error).

Inputs

| Arg | Required | Description | |-----|----------|-------------| | target | No | File or directory to review | | --scope | No | `sorry`, `deps`, `file`, `changed`, or `project` | | --line | No | Line number for single-sorry scope | | --codex | No | External review via Codex (interactive handoff) | | --llm | No | Use llm CLI with model | | --hook | No | Run custom analysis script | | --json | No | Output structured JSON for external tools | | --mode | No | `batch` (default) or `stuck` (triage) | | --mathlib-review | No | Force the Layer-2 mathlib-review bar at full strictness, overriding project-context detection. Mutually exclusive with `--no-mathlib-review`. | | --no-mathlib-review | No | Force Layer-2 findings to advisory, overriding project-context detection. Mutually exclusive with `--mathlib-review`. |

Scope Behavior

**Scope levels:** | Scope | Description | |-------|-------------| | `sorry` | Single sorry at --line (requires target file + --line) | | `deps` | Sorry + same-file helpers and directly referenced lemmas (requires target file + --line) | | `file` | All sorries in target file | | `changed` | Files modified since last commit (git diff) | | `project` | Entire project (requires confirmation) |

**Defaults:**

• No args → `--scope=changed`
• Target file provided → `--scope=file`
• Target + `--line` → `--scope=sorry`
• Triggered by prove/autoprove → matches current focus (`sorry` or `file`)

**Note:** Scope filtering is implemented by the reviewing agent, not the underlying scripts. The agent reads script output and filters results to match the requested scope.

**Project-wide confirmation:**

⚠️  This will review the entire project.
Proceed? (yes / no)

**Output header always shows scope:**

## Lean4 Review Report
**Scope:** Core.lean:89 (single sorry)

Review Modes

**Batch mode (default):**

• Purpose: "What changed in this batch" + basic hygiene — full review report with all sections
• Use: Regular cadence reviews, manual quality checks

**Stuck mode:**

• Trigger: prove/autoprove invokes stuck mode per its detection triggers when no progress is detected. Can also be invoked manually.
• Purpose: "What's blocking progress on current focus" — top 3 blockers with actionable next steps
• Lightweight: Skips full golf analysis and complexity metrics; focuses on blockers only

**Stuck mode output format:**

## Stuck Review — Core.lean:89

**Primary blocker class:** missing library lemma

**Top 3 blockers:**
1. Missing lemma about tendsto_atTop → search Mathlib.Topology.Order
2. Typeclass instance missing for MeasurableSpace β → supply the intended structure (`have : MeasurableSpace β := borel β` only when `[TopologicalSpace β]` is available and Borel is intended; otherwise import the declaring module or report the missing prerequisite); `inferInstance` would re-run the failed search
3. Proof too long (38 lines) → extract helper lemma first

**Evidence:**
- searches — `lean_leansearch "tendsto atTop of monotone"`, `lean_loogle "Tendsto _ atTop"`
- returned lemmas — `tendsto_atTop_mono`, `Tendsto.comp`
- attempts — `exact tendsto_atTop_mono h` (type mismatch), `apply Tendsto.comp` (unification goal)

**Flag:** Statement may be false (optional — see below)

**Recommended next action:** Search for tendsto variants in Topology/Order
**Why first:** the top blocker is a missing lemma, so search dominates more tactic attempts
**next_action:** continue

The **Primary blocker class** value uses the Blocked-Goal Triage vocabulary from [sorry-filling.md](../skills/lean4/references/sorry-filling.md) (definitional equality / missing intro-constructor-cases / missing rewrite / arithmetic / missing library lemma / typeclass-coercion-elaboration / needs helper lemma) and classifies the top blocker — the listed blockers may span classes. The **Evidence** block records the searches attempted