mcpField
L
loogle-search

loogle-search

github.com/parcadei开发3.9k487 次安装39 周前更新
代码仓库

关于 loogle-search

通过类型签名模式搜索 Mathlib 引理的命令行工具。适用于知道类型形状但不知道引理名称的 Lean 用户。

主要功能

  1. 01按类型模式搜索引理
  2. 02支持类型变量和通配符
  3. 03匹配多个指定词项
  4. 04输出 JSON 结果
  5. 05可连接运行中的服务或直接搜索

适用场景

  1. 01按预期类型查找引理
  2. 02探索包含指定标识符的结果
  3. 03为 Lean 证明查找可应用的结论

安装

复制下面的命令，在终端中运行。

$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, Bar必须同时包含 Foo 和 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–200 ms
  • 冷启动（服务未运行）：每次查询约 10 s（加载 343 MB 索引）

设置

必须先构建 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