Lean 4 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.

Quick Start

Host	Recommended installation	What you get	Details
Claude Code	Native plugin (Tier 3)	Skill + /lean4:* commands, hooks, guardrails, subagents, helper runtime	Claude Code
Codex	Native plugin (Tier 3)	Skill + trusted hooks + absolute-path helper runtime; no /lean4:* parity	Codex
Other Agent Skills hosts (Gemini, Antigravity, Copilot, Cursor, Windsurf, OpenCode, …)	Skill-only quick install	Instructions + references (documented, not CI-verified)	Installation guide
Any host, full runtime	Portable checkout (Tier 2)	Skill + wrappers + helper scripts	Portable

Claude Code (run in chat):

/plugin marketplace add cameronfreer/lean4-skills
/plugin install lean4

Codex (in your shell):

codex plugin marketplace add cameronfreer/lean4-skills --ref main
codex plugin add lean4@lean4-skills

Host-native skill installers generally provide the instructions and references only. Use the portable runtime when you also need the bundled wrappers and scripts; Claude Code and Codex provide native full-plugin installations.

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 explicit stop budgets
disprove	Guided counterexample search with certified refutation
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
diagnose	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. Use disprove instead of prove to refute a statement rather than prove it.

CLI-like inputs to the seven parameter-heavy commands are validated by a host-agnostic parser — see the Command Invocation Contract.

The Shared Proof Cycle

The proving workflows (prove, autoprove, formalize, and autoformalize) share one cycle — Plan → Work → Checkpoint → Review → Replan → Continue/Stop — where each sorry gets a mathlib search, tactic attempts, and validation, and being stuck forces a review + replan. Statement and header changes belong to the synthesis workflows (formalize / autoformalize); prove and autoprove keep declaration headers immutable. Editing .lean files without a command runs one bounded pass — fix the immediate issue, then hand off to the right workflow — with the Blocked-Goal Triage loop for a goal that resists it. Details: cycle-engine.md.

Verification

CI gates every PR: full documentation lint, semantic contract suites, hook and wrapper runtime tests on Linux and macOS Bash 3.2, and pinned shellcheck/ruff/mypy/actionlint. Hosts marked "documented" in the Quick Start table follow verified setup patterns but are not CI-tested.

Lean LSP MCP (Optional, Recommended)

The skill works standalone, but pairs best with lean-lsp-mcp: live goal inspection, mathlib search, and typically much faster feedback than repeated full builds. See INSTALLATION.md → MCP Server for registration on any host, including the Claude Code scope trade-off for subagent visibility.

Documentation

• INSTALLATION.md — installation tiers, host sections, MCP setup
• SKILL.md — core skill reference
• Commands — command documentation
• References — cycle engine, mathlib style, proof golfing, tactic patterns, grind, metaprogramming, and more
• lean4-contribute — opt-in helper for filing bug reports, feature requests, and insights from your editor
• CHANGELOG.md — version history
• MIGRATION.md — migrating from v3 (Claude Code)

Contributing

Issues and PRs welcome at https://github.com/cameronfreer/lean4-skills. With the lean4-contribute plugin installed, your agent may suggest filing bug reports, feature requests, or insights at natural stopping points — drafting starts only after you opt in, and every 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.

@software{lean4-skills,
  author = {Cameron Freer},
  title = {Lean 4 {Skills}: Theorem proving skill and workflow pack for {AI} coding agents},
  url = {https://github.com/cameronfreer/lean4-skills},
  month = oct,
  year = {2025}
}