/lean4

name: lean4
description: "Use when editing .lean files, debugging Lean 4 builds (type mismatch, sorry, failed to synthesize instance, axiom warnings, lake build errors), searching mathlib for lemmas, formalizing mathematics in Lean, finding a counterexample to, refuting, or disproving a Lean statement, or learning Lean 4 concepts. Also trigger when the user asks for help with Lean 4, mathlib, or lakefile. Do NOT trigger for Coq/Rocq, Agda, Isabelle, HOL4, Mizar, Idris, Megalodon, or other non-Lean theorem provers."
license: MIT

Lean 4 Theorem Proving

Use this skill whenever you're editing Lean 4 proofs, debugging Lean builds, formalizing mathematics in Lean, or learning Lean 4 concepts. It prioritizes LSP-based inspection and mathlib search, with scripted primitives for sorry analysis, axiom checking, and error parsing.

Core Principles

**Search before prove.** Many mathematical facts already exist in mathlib. Search exhaustively before writing tactics.

**Build incrementally.** Lean's type checker is your test suite—if it compiles with no sorries and standard axioms only, the proof is sound.

**Respect scope.** Follow the user's preference: fill one sorry, its transitive dependencies, all sorries in a file, or everything. Ask if unclear.

**Use 100-character line width for Lean files.** Do not wrap lines at 80 characters — Lean and mathlib convention is 100. If a line fits within 100 characters, keep it on one line. See [mathlib-style](references/mathlib-style.md) for breaking strategies when lines exceed 100.

**Mathlib style quick check.** For ordinary mathematical lambdas, write `fun x ↦ ...` (`\mapsto`), not `fun x => ...`. Use `=>` for `match`/`do` branches and metaprogramming callback idioms. Prefer `show P by tac` for tactic proofs; use `show P from term` only for term proofs. See [mathlib-style](references/mathlib-style.md).

**Preserve statements and signatures — they're the file's contract.** Theorem/lemma statements and type signatures are off-limits unless the user explicitly requests changes; changing them can break callers or alter the theorem being proved. If a proof seems to require changing a statement or adding a custom axiom, stop and discuss first because that changes the contract or the proof's trust basis. Exception: within synthesis wrappers (`/lean4:formalize`, `/lean4:autoformalize`), session-generated declarations may be redrafted under the outer-loop statement-safety rules; see cycle-engine.md.

**Docstrings are scoped by workflow.** Existing docstrings are API. The default is **Rule A** — any workflow that mutates existing declarations follows it unless the user explicitly requests docstring changes:

| Mode | May do | Boundary | |------|--------|----------| | **A — editing existing declarations** (e.g. `/lean4:prove`, `sorry-filler-deep`, golf, refactor, any agent editing existing decls) | adjust inline comments in proof bodies | never rewrite an existing docstring — explicit user request only | | **B — review** (`/lean4:review`) | flag weak/missing docstrings and propose replacement text in the report | read-only — never mutates files | | **C — new-file / new-decl generation** (`/lean4:draft`, `/lean4:formalize`, `/lean4:autoformalize`) | emit module/declaration docstrings on files or declarations it newly creates | existing docstrings stay under Rule A |

Per-command policy lives in each command's doc. The docstring split applies in every project; when the mathlib Template Gate selects the mathlib header, Rule C fills its module-docstring slot — Rule C neither selects nor redefines the [template](references/mathlib-style.md#1-file-header-copyright-module-imports-critical).

Commands

| Command | Purpose | |---------|---------| | `/lean4:draft` | Draft Lean declaration skeletons from informal claims | | `/lean4:formalize` | Interactive formalization — drafting plus guided proving | | `/lean4:autoformalize` | Autonomous end-to-end formalization from informal sources | | `/lean4:prove` | Guided cycle-by-cycle theorem proving with explicit checkpoints | | `/lean4:autoprove` | Autonomous multi-cycle theorem proving with explicit stop budgets | | `/lean4:disprove` | Guided counterexample search with certified refutation | | `/lean4:checkpoint` | Save progress with a safe commit checkpoint | | `/lean4:review` | Read-only code review of Lean proofs | | `/lean4:refactor` | Leverage mathlib, extract helpers, simplify proof strategies | | `/lean4:golf` | Improve Lean proofs for directness, clarity, performance, and brevity | | `/lean4:learn` | Interactive teaching and mathlib exploration | | `/lean4:diagnose` | Diagnostics, cleanup, and migration help |

`/lean4:*` names are the native plugin's command aliases and also serve as stable workflow names throughout this documentation. On hosts without command registration (skill-only or portable installs), invoke the `lean4` skill with your host's normal syntax and ask for the named workflow — e.g., "Use the guided `prove` workflow on `Foo.lean:42`."

This plugin ships a host-agnostic parser (`lib/command_args/`) that covers the parser-decidable startup rules of the seven parameter-heavy commands (`draft`, `learn`, `formalize`, `autoformalize`, `prove`, `autoprove`, `disprove`). A small set of documented startup rules in these commands depend on runtime context (repo- level search, interactive prompting) and are applied by the command after reading the parser's output. The other commands (`checkpoint`, `review`, `refactor`, `golf`, `diagnose`) remain model-parsed. When a host adapter installs the `UserPromptSubmit` hook, the parser runs before the model sees a `/lean4:*` prompt matching one of the seven covered commands, injects a `validated-invocation` block into context, and rejects invalid invocations at the hook level; invocations of the other commands pass through unchanged. Hosts without the hook fall back to model-parsed startup via the shared [command-invocation.md](references/command-invocation