Agent Skills
› parcadei/Continuous-Claude-v3
› loogle-search
loogle-search
GitHub通过类型签名模式在 Mathlib 中搜索引理，辅助 Lean 证明。支持通配符、变量绑定及多条件匹配，提供 CLI 命令和 JSON 输出，可启动服务器加速查询。
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
