Lean 4 Skills
Lean 4 workflow pack for AI coding agents. Gives your agent a structured
prove/review/golf loop, mathlib search, axiom checking, and safety guardrails.
The workflows are host-agnostic — Claude Code, Codex, Gemini CLI, Cursor, and
others all use the same core skill; only the invocation surface differs.
Workflows
| Workflow | Description |
|---|
| draft | Draft Lean declaration skeletons from informal claims |
| formalize | Interactive formalization — drafting plus guided proving |
| autoformalize | Autonomous end-to-end formalization from informal sources |
| prove | Guided cycle-by-cycle theorem proving |
| autoprove | Autonomous multi-cycle proving with stop rules |
| checkpoint | Save point (per-file + project build, axiom check, commit) |
| review | Read-only quality review |
| refactor | Leverage mathlib, extract helpers, simplify proof strategies |
| golf | Improve proofs for directness, clarity, performance, and brevity |
| learn | Interactive teaching and mathlib exploration |
| doctor | Diagnostics and migration help |
Claude Code: invoke as /lean4:<name>. Other hosts: follow the corresponding workflow in SKILL.md.
Typical session: draft (or formalize / autoformalize) → prove (or autoprove) → review → refactor → golf → checkpoint → git push.
How It Works
draft — Skeleton-only drafting from informal claims. Use when you want Lean declarations without a full prove run.formalize — Interactive synthesis. Drafts a skeleton, then runs guided prove cycles with user interaction.autoformalize — Autonomous synthesis. Extracts claims from a source, drafts skeletons, and proves them unattended.prove — Guided proof engine for existing declarations. Asks preferences at startup, prompts before each commit, pauses between cycles.autoprove — Autonomous proof engine for existing declarations. Auto-commits, loops until a stop condition fires (max cycles, max time, or stuck).- The proof engines share one cycle engine: Plan → Work → Checkpoint → Review → Replan → Continue/Stop. Each sorry gets a mathlib search, tactic attempts, and validation.
--commit controls per-fill commit behavior. When stuck, both force a review + replan.
formalize and autoformalize wrap drafting around that same engine. Statement and header changes belong there — prove and autoprove keep declaration headers immutable.- Editing
.lean files without a command activates the skill for one bounded pass — fix the immediate issue, then suggest the right next command: draft / formalize for statement work, prove / autoprove for proof work.
See plugin README for the full command guide.
Installation
Claude Code (native plugin)
/plugin marketplace add cameronfreer/lean4-skills
/plugin install lean4
Optionally, install the contribution helper to draft bug reports, feature requests, or shareable insights from your editor:
/plugin install lean4-contribute
Other Hosts
Clone (shallow) and follow the setup for your host:
git clone --depth 1 https://github.com/cameronfreer/lean4-skills.git
Lean LSP MCP Server (Optional, Highly Recommended)
The skill works standalone, but plays especially well with lean-lsp-mcp — faster mathlib search and sub-second feedback instead of 30+ second lake build cycles. Works with any MCP-capable host.
What you get:
lean_goal — exact goal state at any linelean_local_search / lean_leanfinder / lean_leansearch / lean_loogle — mathlib searchlean_multi_attempt — test multiple tactics in parallellean_hammer_premise — premise suggestions for simp/aesop/grindlean_diagnostic_messages — per-file error/warning check without a full lake build- …and more (hover info, goal-conditioned search, state inspection, etc.)
Claude Code (run from your Lean project root):
# User-scoped — available in all your projects
claude mcp add --transport stdio --scope user lean-lsp -- uvx lean-lsp-mcp
# Or project-scoped — shared via .mcp.json
claude mcp add --transport stdio --scope project lean-lsp -- uvx lean-lsp-mcp