Lean research
USE FOR: per-question Lean 4 research — picking a research method (Mathlib grep / Web / repo grep / sub-agent), running the discovery ladder for Mathlib/Loogle/Reservoir/GitHub/literature lookups, choosing depth (Shallow / Standard / Deep / Exhaustive), emitting a findings + recommended-strategy + Zettel triple, integrating with the Rumsfeld epistemic matrix and the review council, running a typed protocol (M / T / L / S / D / X / E). DO NOT USE FOR: full council convocation (use @research-council); synthesis emission (use @research-synthesis-engine); package adoption or Lake dependency decisions (use @lean-package-research); proof writing (use @lean-proof); review (use @lean-review-council). TRIGGERS: research, mathlib lookup, find lemma, theorem search, Loogle, Moogle, Reservoir, package search, literature search, web search, what does X mean, typed research, M protocol, T protocol, L protocol.From its SKILL.md
npx -y skills add r-irbe/proof-skills --skill lean-researchAssembled from the repository path, not quoted from the project. Check it against their README if it does not work.
One thing to look at
- 2 stars2 stars. Stars are a popularity signal and not a quality one, but at this level it is likely that nobody has read this closely except its author, and you would be relying on your own review.
SKILL.md
6.5 KB, ~1.3k tokens by cl100k_base, as published. Nobody here has run it
Lean 4 Research Skill
Systematic methodology for investigating proof strategies, API availability, tactic behavior, and academic connections during Lean 4 formalization.
Routing
- USE FOR / DO NOT USE FOR / TRIGGERS — see the
descriptionfield in the YAML frontmatter above. Same dispatch contract is restated here for in-skill discovery. - USE FOR: per-question Lean 4 research — picking a research method (Mathlib grep / Web / repo grep / sub-agent), running the discovery ladder for Mathlib/Loogle/Reservoir/GitHub/literature lookups, choosing depth (Shallow / Standard / Deep / Exhaustive), emitting a findings + recommended-strategy + Zettel triple, integrating with the Rumsfeld epistemic matrix and the review council, running a typed protocol (M / T / L / S / D / X / E).
- DO NOT USE FOR: full council convocation (use @research-council); synthesis emission (use @research-synthesis-engine); package adoption or Lake dependency decisions (use @lean-package-research); proof writing (use @lean-proof); review (use @lean-review-council).
- TRIGGERS: research, mathlib lookup, find lemma, theorem search, Loogle, Moogle, Reservoir, package search, literature search, web search, what does X mean, typed research, M protocol, T protocol, L protocol.
Workflow
- Classify the research trigger (handbook Part 1) — confirm research is warranted vs proceeding with current evidence.
- Pick a method (handbook Part 2), a depth level (handbook Part 4), and the applicable discovery-ladder type: Symbol, Package, Literature, or Strategy.
- Run the discovery ladder in
references/discovery-ladder.mdwhenever the answer depends on an existing theorem, package, or literature anchor. Record misses with the negative-result block from that reference. - If the question is typed, switch to the typed protocol (handbook Part 9: M = Mathlib, T = Tactic, L = Literature, S = Strategy, D = Domain, X = Cross-domain, E = Empirical).
- Emit the standard output triple (handbook Part 3): Findings + Recommended Strategy + Zettel notes.
- Hand off the recommended strategy to the consumer skill (handbook Part 7 mapping).
Recovery & STOP
- STOP if findings contradict the Rumsfeld matrix classification (handbook Part 5) — re-classify the question first.
- STOP if Mathlib version drift is suspected — re-verify symbol existence at the current pin per the
verification disciplinememory. - STOP before calling a negative theorem/package result exhaustive unless the discovery ladder's required rungs and query variants are recorded.
- STOP if the question would benefit from cross-disciplinary research (handbook Part 9 X-protocol) — escalate to
@research-council.
Handoffs
- Predecessors:
agent:gateway,skill:lean-proof,skill:lean-proof-review,skill:lean-specification,skill:lean-blueprint. - Successors:
skill:lean-zettelkasten,skill:research-council,skill:research-synthesis-engine,skill:lean-package-research,skill:lean-proof,skill:lean-proof-review.
Detailed reference
Full methodology content (Parts 1–9) lives in
references/lean-research-handbook.md.
Load that file when the skill is convened; the SKILL.md only carries
the dispatch contract and a parts index.
| Section | Topic | Covers |
|---|---|---|
| Part 1 | Research Triggers | When to research vs proceed |
| Part 2 | Research Methods | WebFetch / WebSearch / Mathlib grep / repo grep / sub-agent |
| Part 3 | Research Output Standards | Findings + recommended strategy + Zettel |
| Part 4 | Research Depth Levels | Shallow / Standard / Deep / Exhaustive |
| Part 5 | Epistemic Mapping Integration | Rumsfeld matrix bridge |
| Part 6 | Review Council Integration | Σ/Φ delegation paths |
| Part 7 | Domain Skill Cross-References | Per-domain skill dispatch |
| Part 8 | Research Anti-Patterns | What to avoid |
| Part 9 | Typed Research Protocols (M / T / L / S / D / X / E) | Mathlib / Tactic / Literature / Strategy / Domain / Cross / Empirical |
See also
../../references/lean-research-handbook.md— Full handbook (extracted from this skill)../../references/discovery-ladder.md— Runged Mathlib/Loogle/Reservoir/GitHub/literature lookup protocol../../references/discovery-ladder-evals.md— Evaluation prompts for the discovery ladder../lean-package-research/SKILL.md— Successor for package adoption and Lake dependency decisions../lean-zettelkasten/SKILL.md— Successor../research-council/SKILL.md— Successor../research-synthesis-engine/SKILL.md— Successor../_overrides/lean-proof/SKILL.md— Successor../lean-proof-review/SKILL.md— Successor
What ships with it: 1 file
434 B alongside SKILL.md
tests/
- theorem-search.yaml434 B