loogle-search
Allows developers to find specific mathematical lemmas in Mathlib by querying based on their type signatures.
Install
mkdir -p .claude/skills/loogle-search && curl -L -o skill.zip "https://agentskills.codes/api/skills/download/5909" && unzip -o skill.zip -d .claude/skills/loogle-search && rm skill.zipInstalls to .claude/skills/loogle-search
Activation
This is the description your AI agent reads to decide when to run this skill — the better it matches your request, the more reliably it fires.
Search Mathlib for lemmas by type signature patternKey capabilities
- →Search lemmas by type signature
- →Use wildcards in queries
- →Perform type-directed proof search
- →Query lemma signatures
How it works
The skill searches a pre-built index of Mathlib lemmas using pattern matching on type signatures.
Inputs & outputs
When to use loogle-search
- →Find a lemma when the name is unknown
- →Discover available functions for a specific type
- →Perform type-directed proof search
- →Query lemma signatures for Lean proofs
About this skill
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
When not to use it
- →Searching for non-Mathlib lemmas
- →Queries without type patterns
Prerequisites
Limitations
- →Requires building index
- →Cold start is slow
How it compares
It allows searching by functional type shape, which is more effective than name-based search in complex libraries.
Compared to similar skills
loogle-search side by side with the closest alternatives in the catalog.
| Skill | Installs | Updated | Safety | Difficulty |
|---|---|---|---|---|
| loogle-search (this skill) | 1 | 6mo | Review | Intermediate |
| godot | 1,044 | 5mo | Review | Intermediate |
| software-architecture | 333 | 6mo | No flags | Intermediate |
| drizzle | 238 | 2mo | No flags | Intermediate |
Try saying
Example prompts that trigger this skill in your AI assistant.
More by parcadei
View all by parcadei →You might also like
godot
bfollington
This skill should be used when working on Godot Engine projects. It provides specialized knowledge of Godot's file formats (.gd, .tscn, .tres), architecture patterns (component-based, signal-driven, resource-based), common pitfalls, validation tools, code templates, and CLI workflows. The `godot` command is available for running the game, validating scripts, importing resources, and exporting builds. Use this skill for tasks involving Godot game development, debugging scene/resource files, implementing game systems, or creating new Godot components.
software-architecture
davila7
Guide for quality focused software architecture. This skill should be used when users want to write code, design architecture, analyze code, in any case that relates to software development.
drizzle
lobehub
Drizzle ORM schema and database guide. Use when working with database schemas (src/database/schemas/*), defining tables, creating migrations, or database model code. Triggers on Drizzle schema definition, database migrations, or ORM usage questions.
screenshot-to-code
OneWave-AI
Convert UI screenshots into working HTML/CSS/React/Vue code. Detects design patterns, components, and generates responsive layouts. Use this when users provide screenshots of websites, apps, or UI designs and want code implementation.
zustand
lobehub
Zustand state management guide. Use when working with store code (src/store/**), implementing actions, managing state, or creating slices. Triggers on Zustand store development, state management questions, or action implementation.
codex
Lucklyric
Invoke Codex CLI for complex coding tasks requiring high reasoning capabilities. This skill should be invoked when users explicitly mention "Codex", request complex implementation challenges, advanced reasoning, or need high-reasoning model assistance. Automatically triggers on codex-related requests and supports session continuation for iterative development.