/review

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
• Output: 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. Can also be invoked manually.
• Purpose: "What's blocking progress on current focus"
• Output: Top 3 blockers with actionable next steps
• Use: Triggered by prove/autoprove when no progress detected
• Lightweight: Skips full golf analysis and complexity metrics; focuses on blockers only

Stuck mode output format:

## Stuck Review — Core.lean:89

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

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

**Recommended next action:** Search for tendsto variants in Topology/Order
**next_action:** continue

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_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/sorry_analyzer.py" <target> --format=json --report-only
3. Axiom Check - bash "$LEAN4_SCRIPTS/check_axioms_inline.sh" <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 calls, short struct literals, single-expression tactic lines).
5. Golfing Opportunities - ${LEAN4_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/find_golfable.py" <target> --filter-false-positives
6. Complexity Metrics - Proof sizes, longest proofs, tactic patterns

Stuck mode: Steps 5–6 are skipped; focus is on blockers (steps 1–4) for quick triage.

Output

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

### Build Status
✓ Project compiles

### Sorry Audit (N remaining)
| File | Line | Theorem | Suggestion |
|------|------|---------|------------|
| ... | ... | ... | ... |

### Axiom Status
✓ Standard axioms only

### Style Notes
- [file:line] - [suggestion]

### Golfing Opportunities
- [pattern] → [optimization]

### Recommendations
1. [action item]

External Hooks

Custom hooks receive structured JSON on stdin with file information, sorries, axioms, and build status. They return JSON with a suggestions array.

See review-hook-schema.md for full input/output schemas, examples, and performance tips for rate-limited APIs.

External Review Handoff

When --codex is specified, display context for external review:

─────────────────────────────────────────────────────────
CODEX REVIEW — {scope description}
─────────────────────────────────────────────────────────

[Context based on scope:]
- sorry: ±50 lines around the target sorry
- deps: Target sorry + referenced helpers/lemmas
- file: Full file content
- changed: All modified files (git diff)
- project: Full project (requires confirmation)

If no sorries in scope:
- file: Include top-level definitions + relevant sections
- changed: Include diff + changed file list

To review in Codex CLI:
1. Run `codex` in project directory
2. Type `/review` → select "Review uncommitted changes"
3. Or paste the above context and ask for review

Return suggestions as JSON:
{"suggestions": [{"file": "...", "line": N, "severity": "hint|warning", "message": "..."}]}
─────────────────────────────────────────────────────────

Post-Review Actions

After review completes (internal or external), prompt:

## Review Complete

Would you like me to create an action plan from the review findings?
- [yes] — Enter plan mode with 3-6 step implementation plan
- [no] — End review, return to conversation

If "yes":

1. Enter plan mode
2. Create plan with one task per high-priority suggestion
3. Get user approval before execution
4. Route to the appropriate command (review itself remains read-only):
   • Missing proofs / build blockers → /lean4:prove
   • Strategy simplification opportunities → /lean4:refactor
   • Tactic-level brevity cleanup → /lean4:golf

Note: When --mode=stuck is triggered by prove/autoprove, skip this prompt—the proving command handles the follow-up with its own "Apply this plan? [yes/no]" prompt.

JSON Output Schema

When using --json, output follows this structure:

{
  "version": "1.0",
  "build_status": "passing" | "failing",
  "sorries": [
    {"file": "Core.lean", "line": 89, "theorem": "convergence_main", "goal": "..."}
  ],
  "axioms": {
    "standard": ["propext", "Classical.choice", "Quot.sound"],
    "custom": []
  },
  "style_notes": [
    {"file": "Core.lean", "line": 42, "message": "Consider using field syntax"}
  ],
  "golfing_opportunities": [
    {"file": "Core.lean", "line": 78, "pattern": "have chain", "suggestion": "Inline or extract"}
  ],
  "summary": {
    "total_sorries": 3,
    "total_custom_axioms": 0,
    "style_issues": 2,
    "golf_opportunities": 5
  }
}

Stuck mode only: The summary object includes "next_action": "continue" (or other value) when --mode=stuck. Absent in batch mode.

Codex Integration

Note: Codex CLI's /review command is interactive-only. There's no codex review <sha> CLI command for automation. Two approaches are available:

Option A: Interactive Handoff (Recommended)

1. Run codex in the project directory
2. Type /review and select:
   • "Review uncommitted changes" — for working tree
   • "Review a commit" — select SHA from list
   • "Review against a base branch" — for PR-style diff
3. Copy suggestions back to this session

Tip: Use /diff after /review to see exact file changes.

Option B: SDK Automation (codex exec)

For CI or scripted reviews, use codex exec with a review prompt:

codex exec "Review this Lean 4 proof for correctness, focusing on:
1. Incomplete sorries and proof gaps
2. Type mismatches or missing instances
3. Non-standard axiom usage

$(cat Core.lean)
" --output-schema lean4-review-schema.json -o review-output.json

Schema file (lean4-review-schema.json):

{
  "$schema": "https://json-schema.org/draft/2020-12/schema",
  "type": "object",
  "properties": {
    "suggestions": {
      "type": "array",
      "items": {
        "type": "object",
        "properties": {
          "file": {"type": "string"},
          "line": {"type": "integer"},
          "severity": {"enum": ["hint", "warning"]},
          "category": {"enum": ["sorry", "axiom", "style", "structure"]},
          "message": {"type": "string"}
        },
        "required": ["file", "line", "severity", "message"]
      }
    }
  },
  "required": ["suggestions"]
}

See Codex SDK Cookbook for CI integration patterns.

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

Safety

• Read-only (does not modify files permanently)
• Axiom check temporarily appends #print axioms, then restores
• Does not create commits
• Does not apply fixes

See Also

• /lean4:prove - Guided cycle-by-cycle proving
• /lean4:autoprove - Autonomous multi-cycle proving
• /lean4:golf - Apply golfing optimizations
• mathlib-style.md
• Examples