Lean research types
APM-installable agent skills for Lean 4 and Mathlib4 — proof tactics, math domains, review and research workflows, generic tooling.
npx -y skills add r-irbe/proof-skills --skill lean-research-typesAssembled 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
REDIRECT — the typed research protocols (M/T/L/S/D/X/E) previously hosted here have been folded into `lean-research` Part 9. This stub preserves the slug for Ctrl-F discoverability and incoming cross-references (per the zero-deletions Chesterton protocol).
SKILL.md
1.6 KB, as published. Nobody here has run it
SK-38: Typed Research Protocols (REDIRECT)
This skill no longer hosts its own protocols. Its content has been consolidated as follows so the dispatch matrix lives next to the research methodology it specialises:
| Old section | New home |
|---|---|
| Part 1 Classification + Part 9 Dispatch Matrix | lean-research Part 9.1 + 9.2 |
| Parts 2–8 protocol headlines | lean-research Part 9.2 (one row per type) |
| Per-type output templates | references/research-output-templates.md |
| Part 10 Queue Management | references/research-queue.md |
| Part 3.3 Theorem-search loop | references/theorem-search.md (existing) |
Existing inbound links to "SK-38 / lean-research-types / typed
research protocols" should resolve here and then follow the table
above. Do not add new content to this file — author it in
lean-research Part 9 or the linked references instead.
See also: lean-research (full methodology), lean-proof-review
(Type T dispatch target), lean-enforcement (Type S dispatch target),
lean-specification (Type D dispatch target), epistemic-mapping
(Type E primary), research-council (multi-type fan-out).