Loogle Search

作者 parcadeid07ff4b06b62无许可证3.9K 个星标收录于 2026年10月8日更新于 2026年10月8日仓库8个月前更新

Search Mathlib for lemmas by type signature pattern

仅含说明Software Development Research & Analysis

AI 生成的概览

使用 Loogle 工具按类型签名模式在 Mathlib 中搜索引理。

功能: 该技能说明如何使用 Loogle（面向 Lean Mathlib 库的搜索工具），按类型签名模式而非引理名称进行查询。它记录了查询语法，例如通配符、类型变量和以逗号分隔的名称约束，并给出示例搜索与 JSON 输出。它还介绍如何运行本地 Loogle 服务器以加快查询，以及在 Lean 证明中应用找到的引理。
适用场景: 当你已知所需类型或引理的形状但不知道其名称时，当你想了解某个类型有哪些可用引理时，或在 Lean 中进行类型导向的证明搜索时使用。
运行要求: 需要 Loogle 工具以及构建好的 Loogle 索引（约 343MB）；文档提到用 lake 构建 Loogle，并可选运行本地服务器。该技能不附带脚本，仅提供说明。

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

来源与署名

来源：parcadei/continuous-claude-v3位于.claude/skills/loogle-search提交d07ff4b

许可证：无许可证

内容归原作者所有。SourceWeft 从公开仓库中收录这些内容。

举报或申请下架

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

来源与署名

更多来自 parcadei/continuous-claude-v3 的技能

Tldr Stats

Wiring

Workflow Router

Validate Agent

Tour

Tldr Overview

更多Software Development技能

Playground

M5 Onboard

Cardputer Buddy

Web Design Guidelines

Vercel React Native Skills

Vercel React Best Practices