Skill
code-transform
Code transformation tools for repairing, simplifying, and extracting Lean proofs
@project-numinaInstall SkillResearch
Skill
/search
Search tools for finding Lean theorems, lemmas, and definitions in Mathlib
Install
$ npx -y skills add project-numina/numina-lean-agent --skill search --agent claude-codeHow it fires
How this skill gets triggered: by you, by Claude, or both.
- Fires itselfAuto-invocation. Claude auto-loads it when your prompt matches the work.Auto-invocation is when the right skill fires by itself at the right moment, driven by a FLOW.md router and a hook, instead of you invoking it by name. It is the difference between a skill being installed and a skill actually getting used.Read the full definition →
- You can call itInvoke it directly when you want it.
- Slash command
/search
Context preview
The summary Claude sees to decide when to auto-load this skill.
Search tools for finding Lean theorems, lemmas, and definitions in Mathlib
SKILL.md
search.SKILL.mdname: search description: "Search tools for finding Lean theorems, lemmas, and definitions in Mathlib"
Search Tools
Tools for finding relevant Lean theorems, lemmas, and definitions. All scripts are in `skills/cli/`.
Available Tools
| 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.
Ships withnumina-lean-agent
Paper | Leandex | Demo | Putnam 2025 An agent built on Claude Code for formal theorem proving tasks. We used this system to prove all 12 problems from Putnam 2025, and completed a paper-level formalization of Effective Brascamp-Lieb inequalities.
Get the whole plugin
Other skills on numina-lean-agent.
@project-numinaInstall SkillSkill
llm
LLM-assisted tools for informal proofs, proof strategy discussion, and code simplification
@project-numinaInstall SkillSkill
sorrifier
Isolates failing proof steps by replacing them with `sorry` and extracting them into standalone lemmas to modularize and decouple…
@project-numinaInstall SkillSkill
verification
Verification tools for compiling, validating, and disproving Lean theorems
@project-numinaInstall Skill