lean4

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

• Codex CLI — add to AGENTS.md + env vars. See INSTALLATION.md → Codex
• Gemini CLI — add to GEMINI.md + env vars. See INSTALLATION.md → Gemini
• Cursor — project rules → SKILL.md + env vars. See INSTALLATION.md → Cursor
• Windsurf — project rules → SKILL.md + env vars. See INSTALLATION.md → Windsurf
• OpenCode — copy to .opencode/skills/ + env vars. See INSTALLATION.md → OpenCode
• Other agents — point agent at SKILL.md + env vars. See INSTALLATION.md → Generic

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 line
• lean_local_search / lean_leanfinder / lean_leansearch / lean_loogle — mathlib search
• lean_multi_attempt — test multiple tactics in parallel
• lean_hammer_premise — premise suggestions for simp/aesop/grind
• lean_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