cameronfreer / lean4-skills

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 | Verified save point (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 . **Other hosts:** follow the corresponding workflow in SKILL.md. Typical session: (or / ) → (or ) → → → → → . How It Works • ** ** — Skeleton-only drafting from informal claims. Use when you want Lean declarations without a full prove run. • ** ** — Interactive synthesis. Drafts a skeleton, then runs guided prove cycles with user interaction. • ** ** — Autonomous synthesis. Extracts claims from a source, drafts skeletons, and proves them unattended. • ** ** — Guided proof engine for existing declarations. Asks preferences at startup, prompts before each commit, pauses between cycles. • ** ** — 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. controls per-fill commit behavior. When stuck, both force a review + replan. • and wrap drafting around that same engine. Statement and header changes belong there — and keep declaration headers immutable. • Editing files without a command activates the skill for one bounded pass — fix the immediate issue, then suggest the right next command: / for statement work, / for proof work. See plugin README for the full command guide. Installation Claude Code (native plugin) Optionally, install the contribution helper to draft bug reports, feature requests, or shareable insights from your editor: Other Hosts Clone (shallow) and follow the setup for your host: • **Codex CLI** — add to + env vars. See INSTALLATION.md → Codex • **Gemini CLI** — add to + 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 + 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 cycles. Works with any MCP-capable host. **What you get:** • — exact goal state at any line • / / / — mathlib search • — test multiple tactics in parallel • — premise suggestions for simp/aesop/grind • — per-file error/warning check without a full • …and more (hover info, goal-conditioned search, state inspection, etc.) **Claude Code** (run from your Lean project root): **Other hosts:** See INSTALLATION.md → MCP Server Compatibility | Host | Status | Workflow | |---|---|---| | Claude Code | Full native | SKILL.md + scripts + commands, hooks, guardrails, subagents | | Codex / Gemini / OpenCode | Documented\* | SKILL.md + scripts | | Cursor / Windsurf | Documented\* | Project rules → SKILL.md + scripts | \*Documented setup patterns, not CI-verified. Documentation • INSTALLATION.md - Setup guide **lean4 plugin** • SKILL.md - Core skill reference • Commands - Command documentation • References - cycle engine, mathlib style, proof golfing, tactic patterns, grind, metaprogramming, and more **lean4-contribute plugin** — opt-in helper for filing issues on this repo from your editor • README - Full command guide and privacy details • — draft a bug report (plugin bugs, not Lean/mathlib issues) • — request a workflow the plugin doesn't support yet • — share a reusable pattern or antipattern from your session --- • CHANGELOG.md - Version history • Migrating from v3 (Claude Code): see MIGRATION.md Changelog See CHANGELOG.md for version history. Contributing Issues and PRs welcome at https://github.com/cameronfreer/lean4-skills. If you have the plugin installed, your coding agent may suggest filing bug reports, feature requests, or sharing insights at natural stopping points. Drafting starts only after you opt in; submission has its own separate confirmation. Each draft is shown in full before anything is sent. License & Citation MIT licensed. See LICENSE for more information. Citing this repository is highly appreciated but not required by the license. See also CITATION.cff.