What is loogle-search?

A tool to search Mathlib lemmas by type-signature pattern rather than by name, enabling type-directed discovery.

How do I express type variables and wildcards in a pattern?

Use _ for any single type, ?a, ?b as type variables (same variable means same type), and Foo.bar for an exact lemma name.

How can I speed up queries and organize results?

Run a local server (loogle-server) to keep the index in memory and use --json to parse structured results for automation.

loogle-search

Scanned

npx machina-cli add skill parcadei/Continuous-Claude-v3/loogle-search --openclaw

Files (1)

SKILL.md

2.0 KB

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

Source

git clone https://github.com/parcadei/Continuous-Claude-v3/blob/main/.claude/skills/loogle-search/SKILL.mdView on GitHub

Overview

loogle-search lets you locate Lean mathlib lemmas by the shape of their type signature rather than by name. This type-directed approach is invaluable when you know the desired type pattern but not the exact lemma name, or when you want to explore all lemmas related to a type. It speeds proof search by surfacing relevant results and can output JSON for tooling.

How This Skill Works

Enter a pattern using _ for any type and ?a, ?b as type variables; use Foo.bar for exact names. loogle-search finds lemmas whose type signatures match your pattern. For speed, run a server to keep an index in memory and use --json to get structured results.

When to Use It

You know the type shape but not the lemma name (for example Nontrivial _ ↔ _).
You want to discover all lemmas available for a type, such as all Nontrivial ↔ _ lemmas.
You perform type-directed proof search to find supporting lemmas.
You’re looking for map-like lemmas (e.g., functions that resemble List.map).
You need lemmas related to Fintype.card or to quickly locate a specific named lemma (e.g., Fintype.card or List.map).

Quick Start

Step 1: Pick a pattern that captures the type you know, e.g., "(?a → ?b) → List ?a → List ?b".
Step 2: Run loogle-search with that pattern (optionally add --json) or start loogle-server for speed.
Step 3: Read the results, pick a lemma you can apply, and incorporate it into your Lean proof.

Best Practices

Start with broad patterns using ?a, ?b to capture generic shapes.
Constrain results with Foo, Bar or exact names like Foo.bar to filter noise.
Iterate patterns: switch between a general shape and a narrow one to surface related lemmas.
Use the --json output to parse lemma names, arities, and sources.
Use loogle-server for fast, repeated queries during proof development.

Example Use Cases

loogle-search "Nontrivial _ ↔ _ < Fintype.card _" to surface the lemma linking nontriviality to card.
loogle-search "(?a → ?b) → List ?a → List ?b" to surface map-like lemmas such as List.map and List.pmap.
loogle-search "IsCyclic, center" to find lemmas about cyclic groups and their centers (e.g., commutative_of_cyclic_center_quotient).
loogle-search "Fintype.card" to list lemmas about finite cardinals.
loogle-search "List.map" to locate map-like lemmas or exact matches.

Frequently Asked Questions

Add this skill to your agents