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.

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

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: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: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 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, 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 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.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.

Which Command?

| Situation | Command | |-----------|---------| | Draft a Lean skeleton (skeleton by default) | /lean4:draft | | Draft + prove interactively | /lean4:formalize | | Filling sorries (interactive) | /lean4:prove | | Filling sorries (unattended) | /lean4:autoprove | | Searching for a counterexample to refute a claim | /lean4:disprove | | Save point (per-file + project build, best-effort axiom scan, commit) | /lean4:checkpoint | | Quality check (read-only) | /lean4:review | | Simplify proof strategies (mathlib leverage, helpers) | /lean4:refactor | | Optimizing compiled proofs | /lean4:golf | | New to this project / exploring | /lean4:learn --mode=repo | | Navigating mathlib for a topic | /lean4:learn --mode=mathlib | | Something not working | /lean4:doctor | | Formalize + prove end-to-end (unattended) | /lean4:autoformalize --source=... --claim-select=first --out=... |

Contributing (lean4-contribute plugin)

If the lean4-contribute plugin is installed, you may suggest these commands at natural stopping points. Rules:

• Suggest first, never invoke unprompted. Offer a one-line question; do not start the command flow.
• Only invoke after explicit user opt-in in the current conversation. Silence, topic change, or implicit frustration do not count as consent.
• At most once per topic per session unless the user engages.
• Never mid-proof. Wait for a natural stopping point.

| Situation | Suggest | |-----------|---------| | Problem appears to be in lean4-skills itself (wrong command behavior, contradictory docs, broken lint, bad guardrail, confusing plugin UX) — not ordinary Lean/mathlib/user-proof problems | "This looks like a lean4-skills bug. Want me to draft a bug report?" → /lean4-contribute:bug-report | | User wants a workflow the plugin doesn't support, says a command should behave differently, or you must recommend awkward manual steps due to a missing feature | "This looks like a plugin workflow gap. Want me to draft a feature request?" → /lean4-contribute:feature-request | | Result seems reusable beyond the current task: tactic-selection heuristic, mathlib search pattern, anti-pattern, documentation gap with a clear lesson — not one-off theorem facts or private repo details | "That seems reusable beyond this task. Want me to draft a shareable insight?" → /lean4-contribute:share-insight |

If the plugin is not installed and the user clearly hit a lean4-skills bug, workflow gap, or reusable insight (same criteria as above — not ordinary Lean/mathlib issues), you may offer the install hint once:

• At most once per session. Do not repeat if the user declined, ignored it, or moved on.
• Never mid-proof or during an active debugging loop.
• One short line, not a pitch: "If you want, install the lean4-contribute plugin and I can draft that report for you here." See the [lean4-contribute README](../../../../plugins/lean4-contribute/README.md#installation) for setup.

Typical Workflow

┌─ Entry points (pick one) ──────────────────────────────────────────────────────────┐
│ /lean4:draft              Skeleton by default (--mode=attempt for shallow proof)   │
│ /lean4:formalize          Interactive: draft + guided proving                      │
│ /lean4:autoformalize      Autonomous: draft + autonomous proving                   │
└────────────────────────────────────────────────────────────────────────────────────┘
        ↓ (if sorries remain)
/lean4:prove / autoprove    Proof engines (sorry filling, no header edits)
        ↓
/lean4:refactor            Leverage mathlib, extract helpers (optional)
        ↓
/lean4:golf                Improve proofs (optional)
        ↓
/lean4:checkpoint          Save point (per-file + project build)

Use /lean4:learn at any point to explore repo structure or navigate mathlib. Three entry points: /lean4:draft for skeletons, /lean4:formalize for interactive synthesis (draft + guided proving), /lean4:autoformalize for unattended source-to-proof.

Refutation branch: Use /lean4:disprove when the goal is to refute a statement rather than prove it. Always interactive; runs a 6-phase cycle (Plan → Work → Checkpoint → Review → Accumulate → Continue/Stop) where Phase 1 generates dynamic Step 0 / Step 1 / Step 2 menus seeded by accumulated evidence (Phase 5 — Accumulate — replaces prove's Replan). Each cycle is a widening search pass over the same target. Append-only — it adds a T_counterexample theorem alongside the original sorry, never rewrites the original declaration. Requires Python 3.11+ (registry loader). See [disprove-engine.md](references/disprove-engine.md), incl. its [Implementation Status](references/disprove-engine.md#implementation-status) table (deterministic vs model-mediated vs deferred).

Notes:

• /lean4:prove asks before each cycle; /lean4:autoprove loops autonomously with explicit stop budgets
• Both trigger /lean4:review at configured intervals (--review-every)
• When reviews run (via --review-every), they act as gates: review → replan → continue. In prove, replan requires user approval; in autoprove, replan auto-continues
• Review supports --mode=batch (default) or --mode=stuck (triage); review is always read-only
• /lean4:autoformalize wraps draft+autoprove in a single command (source → claims → skeletons → proofs); replaces autoprove --formalize=auto
• Proof engines (prove/autoprove) never modify declaration headers (header fence)
• /lean4:disprove reports REFUTED only when Lean typechecks the negation; otherwise WITNESS_UNCERTIFIED or INCONCLUSIVE
• If you hit environment issues, run /lean4:doctor to diagnose

LSP Tools (Preferred)

Sub-second feedback and search tools (LeanSearch, Loogle, LeanFinder) via Lean LSP MCP:

lean_goal(file, line)                           # See exact goal
lean_hover_info(file, line, col)                # Understand types
lean_local_search("keyword")                    # Fast local + mathlib (unlimited)
lean_leanfinder("goal or query")                # Semantic, goal-aware (10/30s)
lean_leansearch("natural language")             # Semantic search (3/30s)
lean_loogle("?a → ?b → _")                      # Type-pattern (unlimited if local mode)
lean_hammer_premise(file, line, col)            # Premise suggestions for simp/aesop/grind (3/30s)
lean_state_search(file, line, col)              # Goal-conditioned lemma search (3/30s)
lean_multi_attempt(file, line, snippets=[...])  # Test multiple tactics
lean_diagnostic_messages(file)                  # Per-file error/warning check
lean_code_actions(file, line)                   # Resolve "Try this" suggestions to edits

lean_run_code is for isolated scratch experiments, not a substitute for live proof-state inspection via lean_goal/lean_multi_attempt/lean_diagnostic_messages. Prefer live-file tools when the question depends on actual file context.

Capabilities

| Capability | Required | Check | Fallback | |-----------|----------|-------|----------| | Lean / Lake | yes | lean --version, lake --version | none — run /lean4:doctor | | Python 3 | yes (scripts) | $LEAN4_PYTHON_BIN set by bootstrap | none for script-dependent operations | | $LEAN4_SCRIPTS | yes (set by bootstrap) | echo "$LEAN4_SCRIPTS" | run /lean4:doctor | | Lean LSP MCP | no | try lean_goal on any .lean file | scripts + lake env lean (file-level only) | | lean_run_code | no | try calling it | lake env lean on temp file | | lean_code_actions | no | try calling it | manual "Try this" application | | Subagent dispatch | no | host-dependent | run work in main thread | | Slash commands | no | host-dependent | follow skill instructions directly |

Operating Profiles

The skill adapts to what's available. Determine your profile by checking capabilities above, then follow the corresponding guidance.

full (all capabilities)

MCP + subagents + commands. Full workflow with live goal inspection, tactic testing, and parallel subagent dispatch (requires disjoint owned-file sets per agent, or separate worktrees). Subagents get pre-collected MCP context per [cycle-engine.md § Pre-flight Context](references/cycle-engine.md#pre-flight-context-for-subagent-dispatch). If lean_run_code is unavailable, use /tmp scratch files with lake env lean for isolated experiments.

mcpmainonly (MCP available, no subagent dispatch)

MCP works in the main thread. Run all proof work directly — do not delegate to subagents. All cycle-engine phases execute in-thread. If lean_run_code is unavailable, use /tmp scratch files with lake env lean for isolated experiments.

scripts_only (no MCP, no subagents)

Use $LEAN4_SCRIPTS for search and lake env lean / lake build for validation. Key limitations in this mode:

• No live goal inspection — lean_goal is unavailable; you can read the file and check compilation output, but cannot see proof state at a specific line
• No tactic testing — lean_multi_attempt is unavailable; edits must be validated by compiling the file (lake env lean)
• No real-time diagnostics — lean_diagnostic_messages is unavailable; use lake env lean (from project root) for compilation errors, but feedback is file-level, not line-level
• Search is script-based — lean4-skills-smart-search replaces LSP search tools

This mode is functional for straightforward proofs but significantly slower and less precise than MCP-backed workflows.

review_only (read-only, no edits)

Read proof state and assess quality. No edits, no commits, no subagent dispatch.

File Handling Rules

Scratch-work ladder (in preference order):

1. Live file + MCP tools (lean_goal, lean_multi_attempt, lean_diagnostic_messages)
2. lean_run_code for isolated experiments
3. /tmp scratch files only when lean_run_code is unavailable and the experiment must not touch the live file
4. Never create scratch files in the repo root

File inspection: Use Read and Grep to view source files. Never write Python scripts, temp files, or use cat pipelines just to read lines from a file you already have access to.

Staging: Stage only files touched during the current session. Never use git add -A or broad glob patterns. Print the exact staged set before committing.

See [sorry-filling.md](references/sorry-filling.md) for the full scratch-work preference order.

Core Primitives

| Script | Purpose | Output | |--------|---------|--------| | sorry_analyzer.py | Find sorries with context | text (default), json, markdown, summary | | check_axioms_inline.sh | Best-effort axiom scan (top-level declarations) | text | | smart_search.sh | Multi-source mathlib search | text | | find_golfable.py | Detect optimization patterns | JSON | | find_usages.sh | Find declaration usages | text |

Usage: Invoked by commands automatically. See [references/](references/) for details.

Invocation contract. Preferred model-facing form:

• Use lean4-skills-* wrappers for the supported helper scripts

(lean4-skills-sorry-analyzer, lean4-skills-check-axioms-inline, lean4-skills-find-golfable, lean4-skills-find-exact-candidates, lean4-skills-analyze-let-usage, lean4-skills-find-usages, lean4-skills-search-mathlib, lean4-skills-smart-search, lean4-skills-cycle-tracker). These are bare commands on PATH — no $LEAN4_SCRIPTS, no ${LEAN4_PYTHON_BIN:-python3}, no ~, no command substitution. Stable invocation surface that Claude Code can statically allowlist.

• Report-only calls: add --report-only to

lean4-skills-sorry-analyzer, lean4-skills-check-axioms-inline (and unused_declarations.sh if invoked via env-var fallback) — suppresses exit 1 on findings; real errors still exit 1. Do not use in gate commands like /lean4:checkpoint.

• Keep stderr visible for Lean script invocations (no /dev/null

redirect

…

Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

• Author: cameronfreer
• Source: cameronfreer/lean4-skills
• License: MIT

Install and usage instructions live in the source repository linked above.