Lean blueprint

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

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-blueprint

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: generating Lean blueprint, annotating theorems with @[blueprint], scaffolding blueprint directory, building blueprint LaTeX, rendering blueprint web. DO NOT USE FOR: writing Lean proofs (use @lean-proof), opening Lean/Mathlib PRs (use @lean-pr). TRIGGERS: blueprint, leanblueprint, LeanArchitect, dependency-graph.

SKILL.md

3.8 KB, as published. Nobody here has run it

lean-blueprint

⚠️ MANDATORY (hot-tier): the gates in §Behavioural rules and the Persist step in §Workflow are CI-enforced. Skipping Persist = incomplete, regardless of artefact quality (FSIA-R-11-09).

Routing

USE FOR: generating a navigable formal blueprint from a Lean 4 codebase; annotating definitions and theorems with @[blueprint]; scaffolding blueprint/ with leanblueprint new; building blueprint LaTeX via lake build :blueprint; rendering the dependency graph and web view.
DO NOT USE FOR: authoring new Lean proofs (use @lean-proof); opening Lean/Mathlib PRs (use @lean-pr); editing prose docs (use @lean-doc-improvement).
TRIGGERS: blueprint, leanblueprint, LeanArchitect, dependency-graph.

Behavioural rules (G-*)

G-1 (MUST): The blueprint pipeline MUST run the five stages in order (analyze → annotate → scaffold → extract → render). [Trace: AC-01]
G-2 (MUST): Every @[blueprint] annotation MUST carry a matching LaTeX statement in content.tex. [Trace: AC-02]
G-3 (MUST NOT): The skill MUST NOT mutate files outside blueprint/ and the annotated .lean modules. [Trace: AC-03]
G-4 (SHOULD): The skill SHOULD fan out per-module annotators when ≥6 modules are in scope. [Trace: AC-04]
G-5 (MUST): lake build :blueprint MUST succeed before render. [Trace: AC-05]
G-6 (MUST): leanblueprint pdf and leanblueprint web MUST both produce artefacts under blueprint/. [Trace: AC-06]
G-7 (SHOULD NOT): The skill SHOULD NOT re-annotate modules already carrying complete @[blueprint] coverage. [Trace: AC-07]
G-8 (MUST): On any guard failure the skill MUST escalate per §Recovery & STOP. [Trace: AC-08]

Workflow

Discover [discover] — read inputs, list Lean modules, locate lakefile.lean and prior blueprint/.
Plan [discover] — propose per-module annotator fan-out; STOP if confidence < 80 %.
Annotate [execute] — apply @[blueprint] annotations and LaTeX statements inside owned scope.
Build [execute] — run lake build :blueprint.
Verify [validate] — confirm artefacts exist; max 3 retries then escalate.
Render [execute] — run leanblueprint pdf and leanblueprint web.
Persist [persist] (MANDATORY, FSIA-R-11-09) — commit changes, update state tracker, tick tasks.md. Skipping Persist = incomplete.

Recovery & STOP

lake build :blueprint fails ×3 → STOP, escalate to human.
Scope drift (touch outside blueprint/ or annotated .lean files) → immediate STOP, re-anchor.
Confidence < 80 % on annotation strategy → STOP, ask.
Context degradation signals (≥2 from AGENTS.md) → recommend fresh session.

Handoffs

Predecessors / successors: see FM handoffs (grammar from ADR-0080).
Source spec: specs/lean/blueprint/requirements.md — every G-rule traces to an AC there.
Related ADRs: ADR-0076, ADR-0080.

Common failure modes

AI agents commonly: skip the Persist step; over-annotate stable modules; re-run lake build instead of escalating on third failure. Full registry: GUARDRAILS.md §Agent failure taxonomy.