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

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) |

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 β → add `haveI`
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, top candidate lemmas returned, and `lean_multi_attempt` outcomes required by the cycle-engine stuck-handoff contract, so a stuck review is a valid handoff record on its own. These fields are part of the human-readable report only — the JSON summary schema is unchanged; machine-readable extension is deferred pending the schema work in #115.

**next_action classification (stuck mode):** `continue` (retryable), `deep` (needs escalation), `repair` (compiler blocker), `redraft` (statement-shape blocker), `golf` (sorry-free), `stop` (no path). Informational unless autoprove outer loop is active.

**Falsification flag:** Include when analysis suggests statement may be false:

• Decidable goal that failed `decide` or `native_decide`
• Repeated proof failures with no viable approach
• prove/autoprove passed falsification signal from earlier preflight

Example: `**Flag:** Statement may be false (decidable goal failed decide)`

**Blocker priority (stuck mode):** 1. Build errors/diagnostics in focus 2. Sorries on critical path (target line or its dependencies) 3. Custom axioms introduced in focus 4. Long/fragile proofs (performance risk) 5. Falsification signals (decidable goal that failed `decide`, repeated proof failures)

For strategy-level proof simplification (mathlib leverage, helper extraction, congr-lemma patterns), run `/lean4:refactor` or `/lean4:refactor --dry-run`.

Actions

The agent selects files based on scope, then runs these analyses (per file or directory):

1. **Build Status** - `lake build` (project-wide); for scoped review (`--scope=file`), use `lean_diagnostic_messages(file)` + `lake env lean <path/to/File.lean>` (run from project root) first 2. **Sorry Audit** - `lean4-skills-sorry-analyzer <target> --format=json --report-only` 3. **Axiom Check** - `lean4-skills-check-axioms-inline <target> --report-only` 4. **Style Review** - Check mathlib conventions (naming, structure, tactics, 100-char line width). Flag lines wrapped under 100 chars that fit on one line (common: `mkAppM` c