Loogle Search

作者 parcadeid07ff4b06b62無授權條款3.9K 個星標收錄於 2026年10月8日更新於 2026年10月8日儲存庫8 個月前更新

Search Mathlib for lemmas by type signature pattern

僅含說明Software DevelopmentResearch & 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 &

Query Syntax

PatternMeaning
_Any single type
?a, ?bType variables (same variable = same type)
Foo, BarMust mention both Foo and Bar
Foo.barExact name match

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"

Performance

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

Setup

Loogle must be built first:

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

Integration with Proofs

When stuck in a Lean proof:

  1. Identify what type shape you need
  2. Query Loogle to find the lemma name
  3. 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

來源與署名

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

授權條款： 無授權條款

內容歸原作者所有。SourceWeft 從公開儲存庫中收錄這些內容。

檢舉或申請下架

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

Tldr Stats

parcadei

顯示工作階段 token 用量、API 費用、TLDR 壓縮節省金額與 hook 活動的儀表板。

Data & Analytics3.9K8 個月前更新

Wiring

parcadei

指導驗證已建置的基礎設施元件是否真的被呼叫，而非成為死程式碼。

Software Development3.9K8 個月前更新

Workflow Router

parcadei

將使用者的目標路由到對應的專家代理與資源層級，用於研究、規劃、建置或修復任務。

AI & Agents3.9K8 個月前更新

Validate Agent

parcadei

依據當前最佳實務驗證技術方案中的技術選型，並產出驗證交接文件。

Software Development3.9K8 個月前更新

Tour

parcadei

當使用者詢問能力時，提供友善的入門導覽，概述代理能做什麼。

AI & Agents3.9K8 個月前更新

Tldr Overview

parcadei

使用 TLDR 工具鏈產生節省 token 的專案概覽，涵蓋檔案樹、程式結構、呼叫圖與複雜度。

Software Development3.9K8 個月前更新

更多Software Development技能

Playground

anthropics

精選

建立自成一體的互動式 HTML 遊樂場，包含控制項、即時預覽與可複製的提示詞輸出。

Software Development37K今天更新

M5 Onboard

anthropics

精選

透過 USB 偵測 M5Stack ESP32 開發板，燒錄 UIFlow 2.0 韌體並安裝 MicroPython 應用程式套件。

Software Development37K今天更新

Cardputer Buddy

anthropics

精選

指導迭代 Cardputer-Adv 的 MicroPython 應用程式套件：新增應用程式、透過 USB 序列埠推送檔案、查看日誌並執行 REPL 指令。

Software Development37K今天更新

Web Design Guidelines

vercel-labs

精選

依據從遠端來源取得的 Web Interface Guidelines 審查 UI 程式碼，並以 file:line 形式回報問題。

Software Development32K5 週前更新

Vercel React Native Skills

vercel-labs

精選

React Native 與 Expo 最佳實務規則，涵蓋清單效能、動畫、導覽、UI 模式、狀態與 monorepo 設定。

Software Development32K5 週前更新

Vercel React Best Practices

vercel-labs

精選

Vercel 的 React 與 Next.js 效能指南，以 70 條規則的形式用於撰寫、審查與重構程式碼。

Software Development32K5 週前更新