Search Tools

SkillSearch

Search tools for finding Lean theorems, lemmas, and definitions in Mathlib

Available today. Use it from your connected AI after setup.

No other account needed.

Connect ahel once, and every AI you use reads what you have installed.

Then ask your AI: use the Search Tools skill

What this skill tells your AI

The instructions your AI receives, as published by project-numina/numina-lean-agent in skills/search/SKILL.md and read by ahel’s review.

Tools for finding relevant Lean theorems, lemmas, and definitions. All scripts are in skills/cli/.

Tool	Purpose	When to use
leanexplore	Semantic search by natural language or Lean terms	First choice for any search; max 5 parallel queries
loogle	Pattern-based search by type shape	When you know the type signature pattern
leanfinder	Mathlib semantic search	Alternative semantic search
leansearch	Natural language + Lean term search	Alternative to leanexplore
state-search	Search by proof goal/state	When you have a specific proof state to match
hammer-premise	Premise retrieval for automation	When looking for premises for automated tactics

For full parameters and examples, read the corresponding reference-<tool>.md file in this directory.

Advanced