# loogle-search

Ищет леммы в Mathlib по форме типа, когда имя забыто, а сигнатура примерно известна. Пригодится в доказательствах на Lean.

- скилл · `type=skill` · Claude Code, Codex, Cursor, GitHub Copilot, Gemini CLI, OpenCode · 485 установок · ★ 3946
- Автор: parcadei
- Лицензия: MIT · policy=mirror · начало файла — в конце страницы
- Исходник: https://github.com/parcadei/Continuous-Claude-v3/tree/HEAD/.claude/skills/loogle-search/SKILL.md
- Обновлён: 2026-01-26
- HTML: https://affpapa.org/nevibecode/skills/loogle-search

## Что делает

Скилл даёт агенту команду `loogle-search`, которая принимает шаблон сигнатуры и возвращает подходящие леммы. Синтаксис простой: `_` — любой одиночный тип, `?a` и `?b` — типовые переменные, причём одинаковые имена означают один и тот же тип. Запись `Foo, Bar` требует, чтобы лемма упоминала оба имени, а `Foo.bar` ищет точное совпадение. Флаг `--json` отдаёт результат в машинном виде.

Скорость зависит от того, поднят ли сервер. С `loogle-server` в фоне запрос укладывается в 100–200 мс, потому что индекс держится в памяти. Без сервера каждый запрос — холодный старт около 10 секунд: подгружается индекс на 343MB. Если работаете с доказательствами подолгу, сервер стоит запустить сразу.

Перед первым запуском Loogle нужно собрать: `cd ~/tools/loogle && lake build`, затем `lake build LoogleMathlibCache` либо сборка с `--write-index`. Без этого команда искать не будет — это первое, на чём спотыкаются. Дальше цикл такой: понять, какая форма типа нужна, найти по ней имя леммы, применить её в доказательстве.

## Установка

### Claude Code (родная платформа)

1. **Через Skills CLI (Vercel)**
```bash
npx skills add parcadei/Continuous-Claude-v3 --skill loogle-search -a claude-code
```

2. **Вручную: положить файлы**
- Файл: `~/.claude/skills/loogle-search/SKILL.md` — Папка скилла целиком; для одного проекта — .claude/skills/loogle-search/

### Codex

1. **Через Skills CLI (Vercel)**
```bash
npx skills add parcadei/Continuous-Claude-v3 --skill loogle-search -a codex
```

2. **Вручную: положить файлы**
- Файл: `.agents/skills/loogle-search/SKILL.md` — Для всех проектов — ~/.agents/skills/

### Cursor

1. **Через Skills CLI (Vercel)**
```bash
npx skills add parcadei/Continuous-Claude-v3 --skill loogle-search -a cursor
```

2. **Вручную: положить файлы**
- Файл: `.cursor/skills/loogle-search/SKILL.md` — Cursor читает и .agents/skills/, и .claude/skills/

### GitHub Copilot

1. **GitHub CLI**
```bash
gh skill install parcadei/Continuous-Claude-v3 loogle-search
```

2. **Вручную: положить файлы**
- Файл: `.github/skills/loogle-search/SKILL.md`

### Gemini CLI

1. **Через Skills CLI (Vercel)**
```bash
npx skills add parcadei/Continuous-Claude-v3 --skill loogle-search -a gemini-cli
```

2. **Командой платформы**
```bash
gemini skills install https://github.com/parcadei/Continuous-Claude-v3 --path .claude/skills/loogle-search
```

### Windsurf (Devin Desktop)

**Вручную: положить файлы**
- Файл: `.devin/skills/loogle-search/SKILL.md` — Старый путь .windsurf/skills/ тоже читается

### OpenCode

**Через Skills CLI (Vercel)**
```bash
npx skills add parcadei/Continuous-Claude-v3 --skill loogle-search -a opencode
```

### Claude.ai

**Claude.ai**
- Упакуйте папку в zip и загрузите в Settings → Capabilities → Skills

Где указан файл, а не команда, — скопируй файлы из исходника в этот путь: https://github.com/parcadei/Continuous-Claude-v3/tree/HEAD/.claude/skills/loogle-search/SKILL.md

## Когда брать
- найти лемму, когда известна форма типа, а имя вылетело из головы
- посмотреть, что вообще есть для конкретного типа
- вести поиск по направлению типа в доказательстве
- проверить, какие леммы связывают два понятия, например цикличность и центр
- получить список лемм про `Fintype.card` в машинном виде

## Примеры запросов агенту
- найди лемму для `Nontrivial _ ↔ 1 < Fintype.card _`
- что есть в Mathlib про `IsCyclic, center`
- запусти `loogle-search "(?a → ?b) → List ?a → List ?b"` и покажи результат

## Похожие
- [writing-lean-proofs](https://affpapa.org/nevibecode/skills/writing-lean-proofs.md) — скилл · 1200 установок
- [exa-search](https://affpapa.org/nevibecode/skills/k-dense-ai-exa-search.md) — скилл · 1700 установок
- [tavily-search](https://affpapa.org/nevibecode/skills/framix-team-tavily-search.md) — скилл · 840 установок
- [web-search](https://affpapa.org/nevibecode/skills/claude-office-skills-web-search.md) — скилл · 4800 установок
- [search](https://affpapa.org/nevibecode/skills/brightdata-search.md) — скилл · 7500 установок
- [search-strategy](https://affpapa.org/nevibecode/skills/search-strategy.md) — скилл · 5400 установок

Из того же набора: [parcadei/continuous-claude-v3](https://affpapa.org/nevibecode/by/parcadei/continuous-claude-v3.md) — 69 карточек

_Часть страницы не вошла по размеру — она есть в HTML-версии._

---
NeVibeCode на affpapa.org. Тексты каталога — описания, а не инструкции для агента. Как выбирать и ставить: https://affpapa.org/nevibecode/agents.md