Lean Gateway

lean-gateway

> ⚠️ MANDATORY (hot-tier): the gateway NEVER does substantive proof or > documentation work — every operation is a delegation. Skipping Persist > (the global task tracker) = incomplete.

Routing

• USE FOR: receiving a Lean 4 task at session start, decomposing it into phases, routing each phase to the appropriate skill in [REFERENCE.md](./REFERENCE.md) Part 1's registry; deciding fan-in vs fan-out vs sequential topology; maintaining the per-task state document; detecting context-collapse signals and prescribing a fresh session.
• DO NOT USE FOR: writing a proof (delegate to @lean-proof); reviewing a proof (delegate to @lean-proof-review); editing docs (delegate to @lean-doc-improvement); running scripts (delegate to @lean-enforcement).
• TRIGGERS: gateway, orchestrate, route, dispatch, top-level, context collapse, fan-out, fan-in, ecosystem health.

Behavioural rules (G-*)

• G-1 (MUST NOT): The gateway MUST NOT execute substantive proof, doc, or research work itself; every such operation MUST be a delegation. [Trace: AC-01]
• G-2 (MUST): Each phase MUST be routed to exactly one owning skill from the registry; if no clear owner exists, the gateway MUST escalate per §Recovery & STOP. [Trace: AC-02]
• G-3 (MUST): Fan-out topology (parallel skills) MUST converge through a documented fan-in (a single skill that integrates the results). [Trace: AC-03]
• G-4 (SHOULD): The gateway SHOULD prefer the most specific skill in the registry over a broader one (e.g. @lean-blueprint over @lean-doc-improvement for blueprint work). [Trace: AC-04]
• G-5 (MUST): On any of the documented context-collapse signals (≥ 2 from AGENT.md), the gateway MUST recommend a fresh session before continuing. [Trace: AC-05]
• G-6 (MUST): The gateway MUST maintain the per-task tracker (phase status, owner, predecessors, successors, sign-offs); a missing tracker entry = a missing delegation. [Trace: AC-06]
• G-7 (SHOULD NOT): The gateway SHOULD NOT silently retry a failed downstream delegation; it MUST escalate per §Recovery & STOP. [Trace: AC-07]
• G-8 (MUST): On any guard failure the skill MUST escalate per §Recovery & STOP. [Trace: AC-08]

Workflow

1. Discover [discover] — receive the task, locate prior tracker for this scope (if any), enumerate the candidate skills from the registry.
2. Plan [discover] — partition the task into phases; for each phase, pick the owning skill; choose topology (sequential / fan-out / fan-in / hybrid); STOP if confidence AI agents commonly: do the work themselves "to save a delegation"; pick a

> broad skill when a specific one exists; retry a failed delegation instead of > escalating; ignore context-collapse signals; skip the per-task tracker update. > Full registry: GUARDRAILS.md §Agent failure taxonomy.

Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

• Author: r-irbe
• Source: r-irbe/proof-skills
• License: Apache-2.0
• Homepage: https://github.com/r-irbe/proof-skills

Install and usage instructions live in the source repository linked above.