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
Review the instructions the agent will receive before you install.
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
No reviews yet. Tell others what you thought.
No login needed. Share how it worked for you, ask a question, or note where it did not run.
No comments yet. Be the first to write one.
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.