Use when editing .lean files, debugging Lean 4 builds (type mismatch, sorry, failed to synthesize instance, axiom warnings, lake build errors), searching mathlib for lemmas, formalizing mathematics in Lean, or learning Lean 4 concepts. Also trigger when the user asks for help with Lean 4, mathlib, or lakefile. Do NOT trigger for Coq, Agda, Isabelle, or other non-Lean proof assistants.
npx claudepluginhub cameronfreer/lean4-skillsThis skill inherits all available tools. When active, it can use any tool Claude has access to.
references/agent-workflows.mdreferences/axiom-elimination.mdreferences/calc-patterns.mdreferences/command-examples.mdreferences/compilation-errors.mdreferences/compiler-guided-repair.mdreferences/cycle-engine.mdreferences/domain-patterns.mdreferences/ffi-patterns.mdreferences/grind-tactic.mdreferences/instance-pollution.mdreferences/lean-lsp-server.mdreferences/lean-lsp-tools-api.mdreferences/lean-phrasebook.mdreferences/lean4-custom-syntax.mdreferences/learn-pathways.mdreferences/linter-authoring.mdreferences/mathlib-guide.mdreferences/mathlib-style.mdreferences/measure-theory.mdUse this skill whenever you're editing Lean 4 proofs, debugging Lean builds, formalizing mathematics in Lean, or learning Lean 4 concepts. It prioritizes LSP-based inspection and mathlib search, with scripted primitives for sorry analysis, axiom checking, and error parsing.
Search before prove. Many mathematical facts already exist in mathlib. Search exhaustively before writing tactics.
Build incrementally. Lean's type checker is your test suite—if it compiles with no sorries and standard axioms only, the proof is sound.
Respect scope. Follow the user's preference: fill one sorry, its transitive dependencies, all sorries in a file, or everything. Ask if unclear.
Never change statements or add axioms without explicit permission. Theorem/lemma statements, type signatures, and docstrings are off-limits unless the user requests changes. Inline comments may be adjusted; docstrings may not (they're part of the API). Custom axioms require explicit approval—if a proof seems to need one, stop and discuss.
| Command | Purpose |
|---|---|
/lean4:formalize | Turn informal math into Lean statements |
/lean4:prove | Guided cycle-by-cycle theorem proving |
/lean4:autoprove | Autonomous multi-cycle proving with stop rules |
/lean4:checkpoint | Verified save point (build + axiom check + commit) |
/lean4:review | Quality audit (--mode=batch or --mode=stuck) |
/lean4:golf | Optimize proofs for brevity |
/lean4:learn | Interactive teaching and mathlib exploration |
/lean4:doctor | Plugin troubleshooting and migration help |
| Situation | Command |
|---|---|
| Draft a Lean statement from an informal claim | /lean4:formalize |
| Filling sorries (interactive) | /lean4:prove |
| Filling sorries (unattended) | /lean4:autoprove |
| Verified save point | /lean4:checkpoint |
| Quality check (read-only) | /lean4:review |
| Optimizing compiled proofs | /lean4:golf |
| New to this project / exploring | /lean4:learn --mode=repo |
| Navigating mathlib for a topic | /lean4:learn --mode=mathlib |
| Something not working | /lean4:doctor |
/lean4:prove Guided cycle-by-cycle proving (asks before each cycle)
/lean4:autoprove Autonomous multi-cycle proving (runs with stop rules)
↓
/lean4:golf Optimize proofs (optional, prompted at end)
↓
/lean4:checkpoint Create verified save point
Use /lean4:learn at any point to explore repo structure or navigate mathlib. Use /lean4:formalize to turn informal math into Lean statements.
Notes:
/lean4:prove asks before each cycle; /lean4:autoprove loops autonomously with hard stop conditions/lean4:review at configured intervals (--review-every)--review-every), they act as gates: review → replan → approval → continue--mode=batch (default) or --mode=stuck (triage)/lean4:doctor to diagnoseSub-second feedback and search tools (LeanSearch, Loogle, LeanFinder) via Lean LSP MCP:
lean_goal(file, line) # See exact goal
lean_hover_info(file, line, col) # Understand types
lean_local_search("keyword") # Fast local + mathlib (unlimited)
lean_leanfinder("goal or query") # Semantic, goal-aware (10/30s)
lean_leansearch("natural language") # Semantic search (3/30s)
lean_loogle("?a → ?b → _") # Type-pattern (unlimited if local mode)
lean_hammer_premise(file, line, col) # Premise suggestions for simp/aesop/grind (3/30s)
lean_state_search(file, line, col) # Goal-conditioned lemma search (3/30s)
lean_multi_attempt(file, line, snippets=[...]) # Test multiple tactics
| Script | Purpose | Output |
|---|---|---|
sorry_analyzer.py | Find sorries with context | text (default), json, markdown, summary |
check_axioms_inline.sh | Check for non-standard axioms | text |
smart_search.sh | Multi-source mathlib search | text |
find_golfable.py | Detect optimization patterns | JSON |
find_usages.sh | Find declaration usages | text |
Usage: Invoked by commands automatically. See references/ for details.
Invocation contract: Never run bare script names. Always use:
${LEAN4_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/script.py" ...bash "$LEAN4_SCRIPTS/script.sh" ...--report-only to sorry_analyzer.py, check_axioms_inline.sh, unused_declarations.sh — suppresses exit 1 on findings; real errors still exit 1. Do not use in gate commands like /lean4:checkpoint./dev/null redirection), so real errors are not hidden.If $LEAN4_SCRIPTS is unset or missing, run /lean4:doctor and stay LSP-only until resolved.
/lean4:prove and /lean4:autoprove handle most tasks:
Both share the same cycle engine (plan → work → checkpoint → review → replan → continue/stop) and follow the LSP-first protocol: LSP tools are normative for discovery and search; script fallback only when LSP is unavailable or exhausted. Compiler-guided repair is escalation-only — not the first response to build errors. For complex proofs, they may delegate to internal workflows for deep sorry-filling (with snapshot, rollback, and scope budgets), proof repair, or axiom elimination. You don't invoke these directly.
When editing .lean files without invoking a command, the skill runs one bounded pass:
lean_goal/lean_diagnostic_messageslean_local_search + lean_leanfinder/lean_leansearch/lean_loogle)lean_diagnostic_messages (no project-gate lake build in this mode)Use
/lean4:provefor guided cycle-by-cycle help. Use/lean4:autoprovefor autonomous cycles with stop safeguards.
A proof is complete when:
lake build passespropext, Classical.choice, Quot.sound)Verification ladder: lean_diagnostic_messages(file) per-edit → lake env lean <path/to/File.lean> file gate (run from project root) → lake build project gate only. See cycle-engine: Build Target Policy.
See compilation-errors for error-by-error guidance (type mismatch, unknown identifier, failed to synthesize, timeout, etc.).
-- Local instance for this proof block
haveI : MeasurableSpace Ω := inferInstance
letI : Fintype α := ⟨...⟩
-- Scoped instances (affects current section)
open scoped Topology MeasureTheory
Order matters: provide outer structures before inner ones.
Try in order (stop on first success):
rfl → simp → ring → linarith → nlinarith → omega → exact? → apply? → grind → aesop
Note: exact?/apply? query mathlib (slow). grind and aesop are powerful but may timeout.
If LSP tools aren't responding, scripts provide fallback for all operations. If environment variables (LEAN4_SCRIPTS, LEAN4_REFS) are missing, run /lean4:doctor to diagnose.
Script environment check:
echo "$LEAN4_SCRIPTS"
ls -l "$LEAN4_SCRIPTS/sorry_analyzer.py"
# One-pass discovery for troubleshooting (human-readable default text):
${LEAN4_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/sorry_analyzer.py" . --report-only
# Structured output (optional): --format=json
# Counts only (optional): --format=summary
Cycle Engine: cycle-engine — shared prove/autoprove logic (stuck, deep mode, falsification, safety)
LSP Tools: lean-lsp-server (quick start), lean-lsp-tools-api (full API — grep ^## for tool names)
Search: mathlib-guide (read when searching for existing lemmas), lean-phrasebook (math→Lean translations)
Errors: compilation-errors (read first for any build error), instance-pollution (typeclass conflicts — grep ## Sub- for patterns), compiler-guided-repair (escalation-only repair — not first-pass)
Tactics: tactics-reference (tactic lookup — grep ^### TacticName), grind-tactic (SMT-style automation — when simp can't close), simp-reference (simp hygiene + custom simprocs), tactic-patterns, calc-patterns
Proof Development: proof-templates, proof-refactoring (28K — grep by topic), sorry-filling
Optimization: proof-golfing (includes safety rules, bounded LSP lemma replacement, bulk rewrites, anti-patterns; escalates to axiom-eliminator), proof-golfing-patterns, performance-optimization (grep by symptom), profiling-workflows (diagnose slow builds/proofs)
Domain: domain-patterns (25K — grep ## Area), measure-theory (28K), axiom-elimination
Style: mathlib-style, verso-docs (Verso doc comment roles and fixups)
Custom Syntax: lean4-custom-syntax (read when building notations, macros, elaborators, or DSLs), metaprogramming-patterns (MetaM/TacticM API — composable blocks, elaborators), scaffold-dsl (copy-paste DSL template)
Quality: linter-authoring (project-specific linter rules), ffi-patterns (C/ObjC bindings via Lake)
Workflows: agent-workflows, subagent-workflows, command-examples, learn-pathways (intent taxonomy, game tracks, source handling)
Internals: review-hook-schema
Expert guidance for Next.js Cache Components and Partial Prerendering (PPR). **PROACTIVE ACTIVATION**: Use this skill automatically when working in Next.js projects that have `cacheComponents: true` in their next.config.ts/next.config.js. When this config is detected, proactively apply Cache Components patterns and best practices to all React Server Component implementations. **DETECTION**: At the start of a session in a Next.js project, check for `cacheComponents: true` in next.config. If enabled, this skill's patterns should guide all component authoring, data fetching, and caching decisions. **USE CASES**: Implementing 'use cache' directive, configuring cache lifetimes with cacheLife(), tagging cached data with cacheTag(), invalidating caches with updateTag()/revalidateTag(), optimizing static vs dynamic content boundaries, debugging cache issues, and reviewing Cache Component implementations.
Creating algorithmic art using p5.js with seeded randomness and interactive parameter exploration. Use this when users request creating art using code, generative art, algorithmic art, flow fields, or particle systems. Create original algorithmic art rather than copying existing artists' work to avoid copyright violations.