# Lean Doc Requirements

> USE FOR: Extract formal requirements from academic papers, technical reports, and design documents. Use when converting informal mathematical claims into Lean 4 theorem specifications. Covers claim extraction from LaTeX sources, equation identification, proposition mapping, hypothesis inference, and requirement traceability from document to formal specification. DO NOT USE FOR: paper update post-Lean (use @lean-doc-improvement); specification design (use @lean-specification); blueprint generation (use @lean-blueprint). TRIGGERS: doc requirements, requirement extraction, informal-to-Lean, claim extraction, paper-to-spec.

- Skill: `r-irbe/lean-doc-requirements` (Agent Skill)
- Install (CLI): `npx skillmds@latest add r-irbe/lean-doc-requirements`
- Raw SKILL.md: https://api.skillmd.com/api/skills/r-irbe/lean-doc-requirements/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: AI & ML
- Author: r-irbe (https://skillmd.com/u/r-irbe)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/r-irbe/lean-doc-requirements

---



# Lean 4 Document-to-Requirements

Extract formal specification requirements from informal documents (papers, reports, specs) and map them to Lean 4 theorem statements.

---

## Routing

- **USE FOR:** Extract formal requirements from academic papers, technical reports, and design documents. Use when converting informal mathematical claims into Lean 4 theorem specifications. Covers claim extraction from LaTeX sources, equation identification, proposition mapping, hypothesis inference, and requirement traceability from document to formal specification.
- **DO NOT USE FOR:** paper update post-Lean (use @lean-doc-improvement); specification design (use @lean-specification); blueprint generation (use @lean-blueprint).
- **TRIGGERS:** doc requirements, requirement extraction, informal-to-Lean, claim extraction, paper-to-spec.

## Workflow

1. Read the source document; identify each informal mathematical claim, its scope, and implicit assumptions.
2. Pick the requirement template from the body matching the claim class (definition, theorem, lemma, tactic-rule).
3. Produce a draft Lean specification (signature only, no proof) with traceability back to the source.
4. Hand off: to `@lean-specification` for the formal spec design, to `@lean-proof` for the proof, to `@lean-zettelkasten`.

## Recovery & STOP

- STOP if the document is being updated FROM Lean — delegate to `@lean-doc-improvement`.
- STOP if claims are too vague to formalise — request HITL clarification.
- STOP if a project-level blueprint is needed — delegate to `@lean-blueprint`.

## Handoffs

- **Predecessors:** `agent:gateway`, `skill:lean-research`.
- **Successors:** `skill:lean-specification`, `skill:lean-proof`, `skill:lean-zettelkasten`.

---

## Detailed reference

Full content for `lean-doc-requirements` lives in
[`references/lean-doc-requirements-handbook.md`](../../references/lean-doc-requirements-handbook.md).
Load that file when the skill is convened; the SKILL.md only carries
the dispatch contract and the parts index.

| Section | Topic |
|---|---|
| Part 1 | Extraction Pipeline |
| Part 2 | Claim Extraction Protocol |
| Part 3 | Hypothesis Inference |
| Part 4 | Batch Extraction Workflow |
| Part 5 | Council Integration |
| Part 6 | Requirements Traceability |

---

## See also

- [`../../references/lean-doc-requirements-handbook.md`](../../references/lean-doc-requirements-handbook.md) — Full handbook (extracted from this skill)
- [`../lean-specification/SKILL.md`](../lean-specification/SKILL.md) — Successor
- [`../_overrides/lean-proof/SKILL.md`](../_overrides/lean-proof/SKILL.md) — Successor
- [`../lean-zettelkasten/SKILL.md`](../lean-zettelkasten/SKILL.md) — Successor