用途：Loogle Search 用于在 Mathlib 中按类型签名模式搜索引理，适合已知类型形状但不知道引理名称、想发现某类型可用引理，或进行类型导向证明搜索的场景。
主要能力：支持模式查询，如 loogle-search "Nontrivial _ ↔ "、loogle-search "(?a → ?b) → List ?a → List ?b"、loogle-search "IsCyclic, center"；支持 --json 输出，如 loogle-search "List.map" --json。查询语法中， 表示任意单一类型，?a、?b 为类型变量（同名即同类型），Foo, Bar 表示必须同时提及两者，Foo.bar 为精确名称匹配。
使用方式：可直接运行 loogle-search 命令；也可先启动服务器 loogle-server & 以将索引保留在内存中加速查询。使用前需先构建 Loogle：cd ~/tools/loogle && lake build，以及 lake build LoogleMathlibCache（或使用 --write-index）。在 Lean 证明中卡住时，可先确定所需类型形状，再用 Loogle 查询引理名，最后在证明中应用该引理。
性能：服务器运行时每次查询约 100-200ms；冷启动（无服务器）每次查询约 10s，需加载 343MB 索引。
限制：资料未提供收费、平台支持范围、索引更新方式及错误处理等细节。