npx skills add smithery/parcadei --skill loogle-search
parcadei/continuous-claude-v3
loogle-search
Search Mathlib for lemmas by type signature pattern
Installation
$
npx skills add parcadei/continuous-claude-v3 --skill loogle-search
Also in this package
Other skills from parcadei/continuous-claude-v3 · top by installs.
npx skills add parcadei/continuous-claude-v3
More details
Agent compatibility
Declared targets from SKILL.md / docs. Unmarked agents are not listed — the skill may still install via the CLI.
Claude Code
Not declared
Cursor
Not declared
Codex
Not declared
GitHub Copilot
Not declared
Windsurf
Not declared
Gemini CLI
Not declared
Cline
Not declared
OpenCode
Not declared
Also listed on
Alternate registries and mirrors of this skill.
Repository health
Stars
3.9K
License
LICENSE
Default branch
main
Open issues
30
Status
Active
Package contents
Files included with this skill beyond the listing page.
-
skill md
SKILL.md2,014 B -
docs
SUMMARY.md1,972 B
History
- First seen on skills.sh
- First recorded snapshot · 477 installs
SKILL.md
Loogle Search - Mathlib Type Signature Search
Search Mathlib for lemmas by type signature pattern.
When to Use
- Finding a lemma when you know the type shape but not the name
- Discovering what's available for a type (e.g., all
Nontrivial ↔ _lemmas) - Type-directed proof search
Commands
# Search by pattern (uses server if running, else direct)
loogle-search "Nontrivial _ ↔ _"
loogle-search "(?a → ?b) → List ?a → List ?b"
loogle-search "IsCyclic, center"
# JSON output
loogle-search "List.map" --json
# Start server for fast queries (keeps index in memory)
loogle-server &Query Syntax
| Pattern | Meaning |
|---|---|
_ |
Any single type |
?a, ?b |
Type variables (same variable = same type) |
Foo, Bar |
Must mention both Foo and Bar |
Foo.bar |
Exact name match |
Examples
# Find lemmas relating Nontrivial and cardinality
loogle-search "Nontrivial _ ↔ _ < Fintype.card _"
# Find map-like functions
loogle-search "(?a → ?b) → List ?a → List ?b"
# → List.map, List.pmap, ...
# Find everything about cyclic groups and center
loogle-search "IsCyclic, center"
# → commutative_of_cyclic_center_quotient, ...
# Find Fintype.card lemmas
loogle-search "Fintype.card"Performance
- With server running: ~100-200ms per query
- Cold start (no server): ~10s per query (loads 343MB index)
Setup
Loogle must be built first:
cd ~/tools/loogle && lake build
lake build LoogleMathlibCache # or use --write-indexIntegration with Proofs
When stuck in a Lean proof:
- Identify what type shape you need
- Query Loogle to find the lemma name
- Apply the lemma in your proof
-- Goal: Nontrivial G from 1 < Fintype.card G
-- Query: loogle-search "Nontrivial _ ↔ 1 < Fintype.card _"
-- Found: Fintype.one_lt_card_iff_nontrivial
exact Fintype.one_lt_card_iff_nontrivial.mpr h