Skip to the rows

agentsclimarketplace

Epistemic discovery engine

Skill r-irbe/proof-skills/skills/epistemic-discovery-engine

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 epistemic-discovery-engine

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: epistemic discovery — picking a discovery mode (Census / Dependency / Literature / Cross-domain / Community), running an Unknown-Unknown (UU) hunting protocol at the right depth (Shallow / Standard / Deep / Exhaustive), emitting census + probe + trigger reports, anti-stagnation mechanisms, project relevance scoring. DO NOT USE FOR: a known research question (use @lean-research); council convocation on a known artifact (use @lean-review-council or @research-council); synthesis emission of known content (use @research-synthesis-engine). TRIGGERS: discovery, unknown unknown, UU hunt, epistemic discovery, census, dependency probe, cross-domain probe, community probe, anti-stagnation.

SKILL.md

4.9 KB, as published. Nobody here has run it

Epistemic Discovery Engine — Active UU Hunting

The Discovery Engine is the operational arm of epistemic-mapping. Where epistemic-mapping defines quadrants, scores, and transitions, the Discovery Engine executes the search protocols that keep the epistemic map current and the UU zone shrinking.

epistemic-mapping (the map) ←──updates──← epistemic-discovery-engine (the explorer)
research-council  (the strategists)  ←──feeds──← epistemic-discovery-engine (the scout)

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: epistemic discovery — picking a discovery mode (Census / Dependency / Literature / Cross-domain / Community), running an Unknown-Unknown (UU) hunting protocol at the right depth (Shallow / Standard / Deep / Exhaustive), emitting census + probe + trigger reports, anti-stagnation mechanisms, project relevance scoring.
DO NOT USE FOR: a known research question (use @lean-research); council convocation on a known artifact (use @lean-review-council or @research-council); synthesis emission of known content (use @research-synthesis-engine).
TRIGGERS: discovery, unknown unknown, UU hunt, epistemic discovery, census, dependency probe, cross-domain probe, community probe, anti-stagnation.

Workflow

Pick the discovery mode (handbook Part 1) that matches the suspected blind spot.
Run the UU hunting protocol at the chosen depth (handbook Part 2).
Emit the corresponding report (handbook Part 3 — Census / Probe / Trigger templates).
Hand off promising leads to @research-council (deep) or @lean-research (single-question) per handbook Part 4.
Apply anti-stagnation mechanisms (handbook Part 5) when consecutive discovery sessions produce overlapping leads.

Recovery & STOP

STOP if the suspected unknown turns out to be a known-unknown after probe — re-classify and delegate to @lean-research.
STOP if 3+ consecutive sessions in the same mode produce overlapping leads — switch mode per handbook Part 5.
STOP if project relevance score (handbook Part 6) falls below threshold — close the discovery and document the negative result.

Handoffs

Predecessors: agent:gateway, skill:research-council, skill:lean-research.
Successors: skill:research-council, skill:research-synthesis-engine, skill:lean-zettelkasten.

Detailed reference

Full methodology content (Parts 1–7) lives in references/epistemic-discovery-engine-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	Discovery Modes	Census / Dependency / Literature / Cross-domain / Community
Part 2	UU Hunting Protocols	Unknown-unknown probing per level
Part 3	Reporting and Outputs	Census + probe + trigger templates
Part 4	Integration Architecture	Wiring with research-council + synthesis
Part 5	Anti-Stagnation Mechanisms	Discovery-loop diversifiers
Part 6	Applicability Scoring	Per-repository applicability scoring
Part 7	Cross-References	Sibling skill inventory

See also

../../references/epistemic-discovery-engine-handbook.md — Full handbook (extracted from this skill)
../research-council/SKILL.md — Successor
../research-synthesis-engine/SKILL.md — Successor
../lean-zettelkasten/SKILL.md — Successor

Keep looking

Skills are one crate of 328,083. Ordering is by how many stacks a row turns up in, so the top of any crate is what has actually been picked rather than what has the most stars.