loogle-search

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Translation

Chinese

Loogle Search - Mathlib Type Signature Search

Loogle 搜索 - Mathlib 类型签名搜索

Search Mathlib for lemmas by type signature pattern.

通过类型签名模式搜索Mathlib中的引理。

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

当你知道引理的类型结构但不知道名称时查找引理
探索某一类型可用的引理（例如，所有
```
Nontrivial ↔ _
```
形式的引理）
基于类型的证明搜索

Commands

命令

bash

undefined

bash

undefined

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

输出JSON格式结果

loogle-search "List.map" --json

Start server for fast queries (keeps index in memory)

启动服务器以实现快速查询（将索引保存在内存中）

loogle-server &

undefined

loogle-server &

undefined

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

模式	含义
`_`	任意单个类型
`?a` , `?b`	类型变量（相同变量表示相同类型）
`Foo, Bar`	必须同时包含 `Foo` 和 `Bar`
`Foo.bar`	精确名称匹配

Examples

示例

bash

undefined

bash

undefined

Find lemmas relating Nontrivial and cardinality

查找关联Nontrivial和基数的引理

loogle-search "Nontrivial _ ↔ _ < Fintype.card _"

Find map-like functions

查找类map函数

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

查找Fintype.card相关引理

loogle-search "Fintype.card"

undefined

loogle-search "Fintype.card"

undefined

Performance

性能

With server running: ~100-200ms per query
Cold start (no server): ~10s per query (loads 343MB index)

服务器运行时：每次查询约100-200毫秒
冷启动（无服务器）：每次查询约10秒（加载343MB的索引）

Setup

安装配置

Loogle must be built first:

bash

cd ~/tools/loogle && lake build
lake build LoogleMathlibCache  # or use --write-index

必须先构建Loogle：

bash

cd ~/tools/loogle && lake build
lake build LoogleMathlibCache  # 或使用--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

lean

-- 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

当在Lean证明中遇到瓶颈时：

确定你需要的类型结构
查询Loogle以找到引理名称
在证明中应用该引理

lean

-- 目标：从1 < Fintype.card G推导出Nontrivial G
-- 查询：loogle-search "Nontrivial _ ↔ 1 < Fintype.card _"
-- 找到：Fintype.one_lt_card_iff_nontrivial
exact Fintype.one_lt_card_iff_nontrivial.mpr h