メニュー
デフォルトでは、最初にソースを確認する Prompt が選択されています。直接コマンドに切り替えるか、ローカルコピーをダウンロードすることもできます。
インストールを決める前に、SKILL.md と SkillsMP に表示されている付属ファイルをお読みください。
Codex または Claude でインストール この Prompt をコピーして Codex、Claude、または他のアシスタントに貼り付けると、Skill ページを確認してインストールできます。
直接コマンドでは確認用 Prompt が省略されます。実行前にソースを確認してください。
npx skills add https://github.com/project-numina/numina-lean-agent --skill searchコマンドは1行のまま表示されます。コピー前に横へスクロールして全体を確認してください。
ローカルで確認しますか？SkillsMP が現在取得できるファイルをダウンロードできます。
Lean 4 theorem proving toolkit: search lemmas, verify proofs, repair/simplify code, and get LLM-assisted informal proofs
LLM-assisted tools for informal proofs, proof strategy discussion, and code simplification
Code transformation tools for repairing, simplifying, and extracting Lean proofs
SOC 職業分類に基づく
SKILL.md を表示中
| name | search |
| description | Search tools for finding Lean theorems, lemmas, and definitions in Mathlib |
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.