Lean 4 theorem proving with guided + autonomous proving, LSP-first workflows, guardrails, and contribution helpers
npx claudepluginhub cameronfreer/lean4-skillsUnified Lean 4 plugin (draft, formalize, autoformalize, prove, autoprove, checkpoint, review, refactor, golf, learn, doctor) — LSP-first, scripts fallback
Draft and submit bug reports, feature requests, and insights for lean4-skills as GitHub issues. Commands may share Lean code snippets with GitHub — review every draft before confirming.
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.
| 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.
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).--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..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.
/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
Clone (shallow) and follow the setup for your host:
git clone --depth 1 https://github.com/cameronfreer/lean4-skills.git
AGENTS.md + env vars. See INSTALLATION.md → CodexGEMINI.md + env vars. See INSTALLATION.md → Gemini.opencode/skills/ + env vars. See INSTALLATION.md → OpenCodeThe 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 buildClaude 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