Stats
Actions
Tags
From lean4-skills-lite
Search Lean 4 libraries (Mathlib, Init, Std, Batteries) for lemmas, theorems, definitions, type classes, notation, and tactics. Invoke BEFORE guessing any Lean/Mathlib name, grep'ing a local mathlib clone, reading mathlib source files, or WebFetch'ing leanprover-community pages. Also invoke when picking premises for simp/aesop/grind, when checking if a lemma exists, or when looking up the canonical name of a known concept. Trigger phrases: 'does mathlib have', 'find lemma', 'what theorem', 'search mathlib', 'is there a lemma for'. Also triggers on loogle query syntax like '?a -> ?b' and on Lean goal text starting with '⊢'. Mathlib is large and naming is non-obvious — assume the lemma exists and search first.
How this skill is triggered — by the user, by Claude, or both
Slash command
/lean4-skills-lite:lean-searchThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
- **Natural language** ("sum of two primes", "commutativity of addition") — **semantic** (queries leansearch)
?a → ?b → List ?a) — loogle⊢ |re z| ≤ ‖z‖) — leanfinder (only for ⊢ goals or Lean expressions; returns null names for plain English)simp/aesop/grind — hammer_premisepython3 <skill-path>/scripts/search.py <api> "<query>"
Examples:
python3 <skill-path>/scripts/search.py semantic "sum of two even numbers is even"
python3 <skill-path>/scripts/search.py loogle "(?a → ?b) → List ?a → List ?b"
python3 <skill-path>/scripts/search.py leanfinder "⊢ |re z| ≤ ‖z‖"
python3 <skill-path>/scripts/search.py state_search "⊢ n + m = m + n"
python3 <skill-path>/scripts/search.py hammer_premise "⊢ n + m = m + n"
Use returned names from state_search/hammer_premise with: simp only [name1, name2], aesop, or grind [name1, name2].
(?a → ?b) → List ?a → List ?b — type shapeReal.sin — by constant name_ * (_ ^ _) — subexpression wildcard|- _ + 0 = _ — search by conclusion only"comm" — name substring match| API | Limit |
|---|---|
| semantic | 3 / 30s |
| loogle | 3 / 30s |
| leanfinder | 10 / 30s |
| state_search | 6 / 30s |
| hammer_premise | 6 / 30s |
Creates, edits, and optimizes skills for Claude Code, including drafting, evaluating with test prompts, iterating on performance, and improving skill descriptions for better triggering accuracy.
npx claudepluginhub szch79/agent-marketplace --plugin lean4-skills-lite