Lean 4 Skills plugin

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