Find lemmas, reusable mathematical results, in Mathlib by matching the type signature you need for a Lean proof. Search with type variables, related terms, or exact names to identify candidates you can apply.
中文简介正在准备中。当前显示英语简介。
Search Mathlib for lemmas by type signature pattern
安装前可以查看交给 AI 代理的指令内容。
Search Mathlib for lemmas by type signature pattern.
Nontrivial ↔ _ lemmas)# 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 &
| Pattern | Meaning |
|---|---|
_ | Any single type |
?a, ?b | Type variables (same variable = same type) |
Foo, Bar | Must mention both Foo and Bar |
Foo.bar | Exact name match |
# 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"
Loogle must be built first:
cd ~/tools/loogle && lake build
lake build LoogleMathlibCache # or use --write-index
When stuck in a Lean proof:
-- 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
还没有评价。欢迎分享你的使用感受。
无需登录即可发表。欢迎分享使用感受、提问，或说明在哪些环境下无法运行。
还没有评论。来写第一条吧。
Coordinate background agents through saved files, keeping lengthy work transcripts out of the main conversation. It defines how to pass results between agents, monitor progress, and verify completed work with tests.
中文简介正在准备中。当前显示英语简介。
Delegate implementation, file reading, and testing to separate agents, then bring concise summaries back to the main conversation. The rules explain when delegation helps and when a small edit is better handled directly.
中文简介正在准备中。当前显示英语简介。
Organize implementation work across research, planning, validation, implementation, and review agents. Each stage passes files to the next, while implementation starts with failing tests and the main conversation coordinates the workflow.
中文简介正在准备中。当前显示英语简介。
Connect Agentica SDK agents to Claude Code CLI through a proxy, an intermediary server. Use setup and debugging guidance to address file permissions, streamed responses, result formatting, and agents reporting success without performing the requested operations.
中文简介正在准备中。当前显示英语简介。
Consult Agentica APIs when building workflows where multiple AI agents cooperate. This reference covers eleven coordination patterns, agent tracking, shared state, handoffs, and ways to combine results, with pointers to detailed API specifications.
中文简介正在准备中。当前显示英语简介。
Write clearer instructions for Agentica and REPL agents by specifying roles, file operations, and output formats. Includes templates for dividing research, coordinating specialists, reviewing solutions, and passing results between agents through files.
中文简介正在准备中。当前显示英语简介。