lean-mathlib-search
CommunityFind Mathlib/Batteries lemmas to close Lean goals
Authormy04337
Version1.0.0
Installs0
System Documentation
What problem does it solve?
This skill helps you locate relevant lemmas in Mathlib/Batteries to close a Lean 4 proof goal, saving time hunting through libraries.
Core Features & Use Cases
- REPL-assisted lemma lookup: quickly search for exact lemmas that resolve a goal.
- Multi-tool workflow: uses exact?, apply?, #leansearch, #loogle, and #check to verify candidates.
- Domain guidance: leverages batteries catalog and search guide to steer discovery.
Quick Start
Search for a lemma that closes your current Lean 4 goal using Mathlib/Batteries.
Dependency Matrix
Required Modules
None requiredComponents
references
💻 Claude Code Installation
Recommended: Let Claude install automatically. Simply copy and paste the text below to Claude Code.
Please help me install this Skill: Name: lean-mathlib-search Download link: https://github.com/my04337/shapez2-in-lean/archive/main.zip#lean-mathlib-search Please download this .zip file, extract it, and install it in the .claude/skills/ directory.
Agent Skills Search Helper
Install a tiny helper to your Agent, search and equip skill from 471,000+ vetted skills library on demand.