Lean4

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

**Never change statements or add axioms without explicit permission.** Theorem/lemma statements, type signatures, and docstrings are off-limits unless the user requests changes. Inline comments may be adjusted; docstrings may not (they're part of the API). Custom axioms require explicit approval—if a proof seems to need one, stop and discuss. 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.

## 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: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:doctor` | Diagnostics, cleanup, and migration help |

This plugin ships a host-agnostic parser (`lib/command_args/`) that covers the
parser-decidable startup rules of the six parameter-heavy commands (`draft`,
`learn`, `formalize`, `autoformalize`, `prove`, `autoprove`). 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`, `doctor`) 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 six 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.md)
contract.
Commands always announce resolved inputs, reject invalid startup configs before
doing work, and treat wall-clock budgets like `--max-total-runtime` as
best-effort.