mcpField
L
loogle-search

loogle-search

github.com/parcadei開発3.9k487 回インストール39 週間前に更新
リポジトリ

loogle-search について

型シグネチャのパターンで Mathlib の補題を検索するコマンドラインツールです。型の形は分かるものの補題名が不明な Lean ユーザーを支援します。

主な機能

  1. 01型パターンによる補題検索
  2. 02型変数とワイルドカードに対応
  3. 03複数の指定語句を照合
  4. 04JSON 出力
  5. 05起動中のサーバーまたは直接検索

活用シーン

  1. 01想定する型から補題を検索
  2. 02指定した識別子を含む結果の調査
  3. 03Lean の証明に適用する定理の特定

インストール

コマンドをコピーしてターミナルで実行します。

$npx skills add https://github.com/parcadei/continuous-claude-v3 --skill loogle-search

インストール後、Claude Code で/loogle-searchを入力して読み込まれたか確認します。

詳細

Loogle 検索 - Mathlib の型シグネチャ検索

型シグネチャのパターンを使って Mathlib の補題を検索します。

使用する場面

  • 型の形はわかっているものの、補題の名前がわからないとき
  • ある型で利用可能なものを調べるとき（例：すべての Nontrivial ↔ _ 補題）
  • 型に基づく証明検索

コマンド

# 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
loogle-search "List.map" --json

# Start server for fast queries (keeps index in memory)
loogle-server &

クエリ構文

パターン意味
_任意の単一の型
?a、?b型変数（同じ変数は同じ型を表します）
Foo, BarFoo と Bar の両方を含む必要があります
Foo.bar名前の完全一致

例

# Find lemmas relating Nontrivial and cardinality
loogle-search "Nontrivial _ ↔ _ < Fintype.card _"

# Find map-like functions
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
loogle-search "Fintype.card"

パフォーマンス

  • サーバー実行中：クエリあたり約100～200ms
  • コールドスタート（サーバーなし）：クエリあたり約10秒（343MBのインデックスを読み込みます）

セットアップ

まず Loogle をビルドする必要があります。

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

証明との連携

Lean の証明で行き詰まったとき：

  1. 必要な型の形を特定します
  2. Loogle にクエリを送り、補題の名前を探します
  3. 証明でその補題を適用します
-- 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

コメント

Markdown 対応