Lean Search Discovery

Community

scottnarmstrong

lean-search-discovery

Use when searching Mathlib for existing declarations, likely theorem names, relevant files, or proof ingredients before attempting a new Lean proof.

Overview

Publisher	scottnarmstrong
Repository	`LeanAutoformalizationSkills`
Skill name	`lean-search-discovery`
Stars	66
Forks	7
Bundled files	3
License	CC-BY-4.0
Links	Skill source Repository

Markdown instructions
A SKILL.md file the model loads on demand, so it only costs tokens when a request actually matches.
Works with any LLM
AI skills are plain Markdown, not provider-specific code, so this works with GPT, Claude, Gemini, Grok, or a local model.
3 bundled files
Scripts, templates, and references the model can read while it works. Files are read-only and never executed.
Open source
Published by scottnarmstrong on GitHub. Read the source before you install it.

Installation

Install the Lean Search Discovery AI skill in TypingMind to use it with any LLM, or drop it into another agent that reads SKILL.md.

Install in TypingMind

TypingMind installs a skill straight from its GitHub folder — it reads SKILL.md, bundles the resource files, and stores the result locally.

Open the app and go to Plugins → Skills.
Choose "Install from GitHub".
Paste the skill folder URL below and confirm.
https://github.com/scottnarmstrong/LeanAutoformalizationSkills/tree/main/skills/lean-search-discovery
Enable the skill in any chat where you want it available.

Store

Installed

Skills

Add skills

Import one or more skills from a public GitHub folder or a local .skill or .zip archive, or SKILL.md file.

From GitHub URLFrom .skill, .zip, or SKILL.md

GitHub repo or folder

https://github.com/scottnarmstrong/LeanAutoformalizationSkills/tree/main/skills/lean-search-discovery

Points to a single skill folder, or any folder that contains multiple skills. Public repos only.

CancelContinue

Plugins → Skills → Add skill → From GitHub URL, then paste the folder URL and press Continue.

Install in another agent

Any agent that reads the Agent Skills format can use this skill — copy the folder into that agent's skills directory.

Claude Code — .claude/skills

git clone --depth 1 https://github.com/scottnarmstrong/LeanAutoformalizationSkills.git /tmp/LeanAutoformalizationSkills
mkdir -p .claude/skills
cp -r /tmp/LeanAutoformalizationSkills/skills/lean-search-discovery .claude/skills/lean-search-discovery

Restart Claude Code after copying so it picks up the new skill.

Use it in TypingMind

Enable Lean Search Discovery in any TypingMind chat and the model takes it from there. Its name and description sit in the system prompt, and the moment a request matches, the model loads the full instructions itself — you never invoke it by hand, and it costs no tokens until it is actually used.

The model loads Lean Search Discovery on its own as soon as a request matches it.

Works with any AI model

AI skills are plain Markdown instructions rather than provider-specific code, so Lean Search Discovery is not tied to the model it was written for. Install it once in TypingMind and use it with GPT-5, Claude, Gemini, Grok, DeepSeek, Mistral, Llama, or a local model you run yourself — all on your own API keys.

Loaded only when it is needed
The system prompt carries just the name and description. The instructions are fetched on the first matching request, so an idle skill costs nothing.
Switch models mid-chat
Because the skill is instructions rather than code, changing model does not break it — the next model reads the same SKILL.md.

Skill instructions

This is the SKILL.md content the model loads. Read it before installing — a skill is instructions your model will follow.

Lean Search Discovery

Use this skill when the next bottleneck is not proving a statement from scratch, but finding the right declaration, namespace, import, or existing theorem. The default posture is: search before you prove.

Search Workflow

Decide what you are searching for.
- a theorem name
- a namespace or file
- a rewrite lemma
- a theorem with a recognizable type signature
Predict likely names from Mathlib conventions.
- use conclusion-driven names such as foo_of_bar
- translate symbols into name fragments like mem, inter, union, nonneg, inj
Search locally first.
- inside Lean: exact?, apply?, rw?, simp?, #check, #print
- in the terminal: rg, find, ls, targeted file inspection
Verify every hit before using it.
- confirm the statement shape
- confirm the namespace and import path
- confirm the lemma is at the right level of generality
Only after two or more search strategies fail should you assume the theorem is missing and start proving it yourself.

Local Search Rules

Prefer rg in .lake/packages/mathlib/Mathlib for terminal search.
Search both likely names and nearby concepts.
Limit output aggressively so inspection stays local and readable.
After a hit, read the surrounding file rather than trusting the name alone.

In-Proof Search Rules

exact? is for “this goal should be one lemma.”
apply? is for “this looks like the head of a useful theorem.”
rw? is for normal-form mismatches.
simp? is for turning exploratory simplification into explicit simp only [...].
None of these should remain in finished code.

Online Search

If online access is available, use Loogle or LeanSearch when local name search is not enough. Treat them as discovery tools, not proof authorities: always verify the result locally with #check, #print, or direct file inspection.

References

Read references/search-and-discovery.md for the full search workflow, theorem-name heuristics, and search-service guidance.
Read references/tools.md when choosing between search tactics, terminal search, API docs, and broader workflow tools.

Bundled files

The model reads these on demand while the skill is loaded. They are exposed as readable files and are never executed.

Frequently asked questions

What does the Lean Search Discovery AI skill do?

Use when searching Mathlib for existing declarations, likely theorem names, relevant files, or proof ingredients before attempting a new Lean proof.

Why use Lean Search Discovery on TypingMind?

Because you install it once and use it with any model. Lean Search Discovery is plain Markdown rather than provider-specific code, so the same skill runs on GPT-5, Claude, Gemini, Grok, or a local model — and you can switch model mid-chat without it breaking. TypingMind runs on your own API keys, so you pay providers directly instead of a per-seat subscription, and your skills and chats stay in your own storage.

How do I install Lean Search Discovery in TypingMind?

Open Plugins → Skills → Install from GitHub in TypingMind and paste https://github.com/scottnarmstrong/LeanAutoformalizationSkills/tree/main/skills/lean-search-discovery. TypingMind reads its SKILL.md and bundles its files and installs it as a skill you can enable per chat.

Which AI models can use Lean Search Discovery?

Any model you connect in TypingMind. AI skills are plain Markdown instructions rather than provider-specific code, so GPT, Claude, Gemini, Grok, and local models can all load this skill when a request matches it.

How many AI models can I use with Lean Search Discovery?

As many as you like. As long as a model supports skills, you can use Lean Search Discovery with it — GPT, Claude, Gemini, Grok, DeepSeek, Mistral, Llama and more — all on TypingMind with your own API keys.

Is the Lean Search Discovery AI skill free?

Yes. It is published on GitHub by scottnarmstrong under the CC-BY-4.0 license. You only pay your own AI provider for the tokens you use.

What are AI skills?

An AI skill is a reusable instruction bundle that teaches an AI model how to do one specific task. It follows the open Agent Skills format: a SKILL.md file with a name and description, plus any scripts, templates or reference files the model may need. The model reads the instructions only when your request matches the skill, so an installed skill costs nothing until it is used.

How are AI skills different from plugins or MCP servers?

A plugin or MCP server gives a model new tools to call — code that runs somewhere and returns a result. An AI skill gives the model knowledge and process instead: how to approach a task, which steps to follow, what good output looks like. Skills are plain Markdown, so they need no server, no API key and no runtime, and they work with any model.

View all

Openclaw Test Performance

openclaw

OrganizationPopular

Benchmark, diagnose, and optimize OpenClaw test and plugin-suite runtime, import hotspots, CPU/RSS, heap growth, and slow coverage paths.

Openclaw Testing

Choose proportional OpenClaw tests and checks, diagnose failures, and route environment-sensitive or release proof to its owner.

Release Openclaw Ci

Run, watch, debug, and summarize OpenClaw full release CI, release checks, live provider gates, install/update proofs, and release-secret preflights.

Release Openclaw Mac

Run or recover OpenClaw macOS release signing, notarization, appcast, and asset promotion.

Overview

Installation

Install in TypingMind

Install in another agent

Use it in TypingMind

Works with any AI model

Skill instructions

Lean Search Discovery

Search Workflow

Local Search Rules

In-Proof Search Rules

Online Search

References

Bundled files

Frequently asked questions

Related AI Skills

Set up your own AI workspace now