# Lean Blueprint

> 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: `r-irbe/lean-blueprint` (Agent Skill)
- Install (CLI): `npx skillmds@latest add r-irbe/lean-blueprint`
- Raw SKILL.md: https://api.skillmd.com/api/skills/r-irbe/lean-blueprint/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- Author: r-irbe (https://skillmd.com/u/r-irbe)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/r-irbe/lean-blueprint

---


# 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

1. **Discover** [discover] — read inputs, list Lean modules, locate `lakefile.lean` and prior `blueprint/`.
2. **Plan** [discover] — propose per-module annotator fan-out; STOP if confidence < 80 %.
3. **Annotate** [execute] — apply `@[blueprint]` annotations and LaTeX statements inside owned scope.
4. **Build** [execute] — run `lake build :blueprint`.
5. **Verify** [validate] — confirm artefacts exist; max 3 retries then escalate.
6. **Render** [execute] — run `leanblueprint pdf` and `leanblueprint web`.
7. **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.