Agent Skills
› parcadei/Continuous-Claude-v3
› loogle-search
loogle-search
GitHub用于在 Mathlib 中通过类型签名模式搜索引理的工具，辅助 Lean 开发进行类型导向的证明搜索。
Trigger Scenarios
需要查找特定类型形状的引理但不知其名称
探索某类型可用的所有引理
在进行 Lean 证明时受阻，需查找匹配类型的引理
Install
npx skills add parcadei/Continuous-Claude-v3 --skill loogle-search -g -y
SKILL.md
Frontmatter
{
"name": "loogle-search",
"description": "Search Mathlib for lemmas by type signature pattern"
}
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-index
Integration 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
Version History
- d07ff4b Current 2026-08-20 12:47
