Loogle Search

by parcadeid07ff4b06b62No license3.9K starsListed Oct 8, 2026Updated Oct 8, 2026Repository updated 8 months ago

Search Mathlib for lemmas by type signature pattern

Instructions onlySoftware Development Research & Analysis

AI-generated overview

Searches Mathlib for lemmas by type signature pattern using the Loogle tool.

What it does: This skill explains how to query Loogle, a search tool for the Lean Mathlib library, using type signature patterns rather than lemma names. It documents the query syntax, such as wildcards, type variables, and comma-separated name constraints, and shows example searches and JSON output. It also covers running a local Loogle server for faster queries and applying found lemmas inside Lean proofs.
When to use it: Use it when you know the shape of a type or lemma you need but not its name, when exploring what lemmas exist for a given type, or when doing type-directed proof search in Lean.
Requirements: Requires the Loogle tool and a built Loogle index (about 343MB); the document mentions building Loogle with lake and optionally running a local server. It ships no scripts, only instructions.

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

bash

# 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 outputloogle-search "List.map" --json
# Start server for fast queries (keeps index in memory)loogle-server &

# 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 outputloogle-search "List.map" --json
# Start server for fast queries (keeps index in memory)loogle-server &

Query Syntax

Examples

bash

# Find lemmas relating Nontrivial and cardinalityloogle-search "Nontrivial _ ↔ _ < Fintype.card _"
# Find map-like functionsloogle-search "(?a → ?b) → List ?a → List ?b"# → List.map, List.pmap, ...
# Find everything about cyclic groups and centerloogle-search "IsCyclic, center"# → commutative_of_cyclic_center_quotient, ...
# Find Fintype.card lemmasloogle-search "Fintype.card"

# Find lemmas relating Nontrivial and cardinalityloogle-search "Nontrivial _ ↔ _ < Fintype.card _"
# Find map-like functionsloogle-search "(?a → ?b) → List ?a → List ?b"# → List.map, List.pmap, ...
# Find everything about cyclic groups and centerloogle-search "IsCyclic, center"# → commutative_of_cyclic_center_quotient, ...
# Find Fintype.card lemmasloogle-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:

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

lean

-- Goal: Nontrivial G from 1 < Fintype.card G-- Query: loogle-search "Nontrivial _ ↔ 1 < Fintype.card _"-- Found: Fintype.one_lt_card_iff_nontrivialexact Fintype.one_lt_card_iff_nontrivial.mpr h

-- Goal: Nontrivial G from 1 < Fintype.card G-- Query: loogle-search "Nontrivial _ ↔ 1 < Fintype.card _"-- Found: Fintype.one_lt_card_iff_nontrivialexact Fintype.one_lt_card_iff_nontrivial.mpr h

Source and attribution

Source:parcadei/continuous-claude-v3in.claude/skills/loogle-searchat commitd07ff4b

License: No license

Content belongs to its original authors. SourceWeft indexes it from a public repository.

Report or request removal

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

Loogle Search

Loogle Search - Mathlib Type Signature Search

When to Use

Commands

Query Syntax

Examples

Performance

Setup

Integration with Proofs

Source and attribution

More from parcadei/continuous-claude-v3

Tldr Stats

Wiring

Workflow Router

Validate Agent

Tour

Tldr Overview

More in Software Development

Playground

M5 Onboard

Cardputer Buddy

Web Design Guidelines

Vercel React Native Skills

Vercel React Best Practices