Lean research

Skill r-irbe/proof-skills/skills/lean-research

APM-installable agent skills for Lean 4 and Mathlib4 — proof tactics, math domains, review and research workflows, generic tooling.

Install

npx -y skills add r-irbe/proof-skills --skill lean-research

Assembled 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.

What its author says it does

Copied from the file, not written here

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.

SKILL.md

6.5 KB, 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 description field 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.md whenever 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 discipline memory.
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