# Lean4

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

- **Type:** Skill
- **Install:** `agentstack add skill-cameronfreer-lean4-skills-lean4`
- **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior
- **Seller:** [cameronfreer](https://agentstack.voostack.com/s/cameronfreer)
- **Installs:** 0
- **Category:** [Agent Skills](https://agentstack.voostack.com/c/agent-skills)
- **Latest version:** 0.1.0
- **License:** MIT
- **Upstream author:** [cameronfreer](https://github.com/cameronfreer)
- **Source:** https://github.com/cameronfreer/lean4-skills/tree/main/plugins/lean4/skills/lean4

## Install

```sh
agentstack add skill-cameronfreer-lean4-skills-lean4
```

Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent.

## About

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

### mcp_main_only (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](https://github.com/cameronfreer)
- **Source:** [cameronfreer/lean4-skills](https://github.com/cameronfreer/lean4-skills)
- **License:** MIT

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

## Pricing

- **Free** — Free

## Security capabilities

Automated source analysis of v0.1.0 — what this tool can access:

- **Network access:** no
- **Filesystem access:** no
- **Shell / process execution:** no
- **Environment & secrets:** no
- **Dynamic code execution:** no

*"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.*


## Versions

- **0.1.0** — security scan: passed — Imported from the upstream source.

## Links

- Listing page: https://agentstack.voostack.com/l/skill-cameronfreer-lean4-skills-lean4
- Seller: https://agentstack.voostack.com/s/cameronfreer
- Browse the marketplace: https://agentstack.voostack.com/browse

---
Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.