How do I install the Lean Specification skill?

Run npx skillmds@latest add r-irbe/lean-specification in your terminal (requires Node.js), paste this page's agent-chat prompt into Claude, Cursor, or any MCP-connected agent, or download the SKILL.md file and copy it into your agent's skills directory.

Is Lean Specification safe to use?

This skill has not completed SkillMD's automated safety review yet. SkillMD never runs a skill's scripts for you; review the SKILL.md before installing.

Which AI agents work with Lean Specification?

This skill is tagged as working with Claude Code, Claude.ai, OpenAI Codex. SKILL.md is an open format, so most agents that read a skills directory can load it too.

Is Lean Specification free to use?

Yes. Installing skills from SkillMD is free, and the skill stays under its author's original license.

Who published Lean Specification?

r-irbe (@r-irbe) published this skill. Their other Agent Skills are listed on their SkillMD profile.

Lean Specification by r-irbe — Agent Skill

Name: Lean Specification
Author: r-irbe

Lean Specification

USE FOR: Design theorem specifications for Lean 4 proofs. Use when planning new theorems, lemmas, definitions, or tactics. Covers the three-part specification (requirements, design, documentation), lifecycle management, dependency analysis, and integration with the review council. DO NOT USE FOR: actual proof writing (use @lean-proof); requirement extraction (use @lean-doc-requirements); review (use @lean-proof-review). TRIGGERS: specification, theorem spec, three-part spec, lemma plan, tactic plan.

r-irbe 06bea37 2.9 KB Updated Sep 17, 2026

File contents

Lean 4 Theorem Specification

Structured process for specifying theorems before implementation. Every theorem passes through Specify → Design → Implement → Review → Merge, with each stage tracked by document templates.

Routing

USE FOR: Design theorem specifications for Lean 4 proofs. Use when planning new theorems, lemmas, definitions, or tactics. Covers the three-part specification (requirements, design, documentation), lifecycle management, dependency analysis, and integration with the review council.
DO NOT USE FOR: actual proof writing (use @lean-proof); requirement extraction (use @lean-doc-requirements); review (use @lean-proof-review).
TRIGGERS: specification, theorem spec, three-part spec, lemma plan, tactic plan.

Workflow

Identify the artifact: new theorem, new lemma, new definition, or new tactic.
Apply the three-part specification template from the body (signature, intent, traceability); verify Mathlib primitives exist at the pin.
Produce the spec; add explicit non-goals + dependencies.
Hand off: to @lean-proof for the proof, to @lean-proof-review once proven, to @lean-zettelkasten.

Recovery & STOP

STOP if the artifact is informal — extract requirements via @lean-doc-requirements first.
STOP if the spec depends on Mathlib primitives missing at the pin — escalate to @lean-research.
STOP if reviewer would reject on grounds the body covers (vacuous truth, missing hypothesis) — fix before publishing.

Handoffs

Predecessors: agent:gateway, skill:lean-research.
Successors: skill:lean-proof, skill:lean-proof-review, skill:lean-zettelkasten.

Detailed reference

Full content for lean-specification lives in references/lean-specification-handbook.md. Load that file when the skill is convened; the SKILL.md only carries the dispatch contract and the parts index.

(See handbook for full content.)

---name: lean-specificationdescription: USE FOR: Design theorem specifications for Lean 4 proofs. Use when planning new theorems, lemmas, definitions, or tactics. Covers the three-part specification (requirements, design, documentation), lifecycle management, dependency analysis, and integration with the review council. DO NOT USE FOR: actual proof writing (use @lean-proof); requirement extraction (use @lean-doc-requirements); review (use @lean-proof-review). TRIGGERS: specification, theorem spec, three-part spec, lemma plan, tactic plan.---# Lean 4 Theorem SpecificationStructured process for specifying theorems before implementation. Every theorem passes through Specify → Design → Implement → Review → Merge, with each stage tracked by document templates.---## Routing- **USE FOR:** Design theorem specifications for Lean 4 proofs. Use when planning new theorems, lemmas, definitions, or tactics. Covers the three-part specification (requirements, design, documentation), lifecycle management, dependency analysis, and integration with the review council.- **DO NOT USE FOR:** actual proof writing (use @lean-proof); requirement extraction (use @lean-doc-requirements); review (use @lean-proof-review).- **TRIGGERS:** specification, theorem spec, three-part spec, lemma plan, tactic plan.## Workflow1. Identify the artifact: new theorem, new lemma, new definition, or new tactic.2. Apply the three-part specification template from the body (signature, intent, traceability); verify Mathlib primitives exist at the pin.3. Produce the spec; add explicit non-goals + dependencies.4. Hand off: to `@lean-proof` for the proof, to `@lean-proof-review` once proven, to `@lean-zettelkasten`.## Recovery & STOP- STOP if the artifact is informal — extract requirements via `@lean-doc-requirements` first.- STOP if the spec depends on Mathlib primitives missing at the pin — escalate to `@lean-research`.- STOP if reviewer would reject on grounds the body covers (vacuous truth, missing hypothesis) — fix before publishing.## Handoffs- **Predecessors:** `agent:gateway`, `skill:lean-research`.- **Successors:** `skill:lean-proof`, `skill:lean-proof-review`, `skill:lean-zettelkasten`.---## Detailed referenceFull content for `lean-specification` lives in[`references/lean-specification-handbook.md`](../../references/lean-specification-handbook.md).Load that file when the skill is convened; the SKILL.md only carriesthe dispatch contract and the parts index._(See handbook for full content.)_---## See also- [`../../references/lean-specification-handbook.md`](../../references/lean-specification-handbook.md) — Full handbook (extracted from this skill)- [`../_overrides/lean-proof/SKILL.md`](../_overrides/lean-proof/SKILL.md) — Successor- [`../lean-proof-review/SKILL.md`](../lean-proof-review/SKILL.md) — Successor- [`../lean-zettelkasten/SKILL.md`](../lean-zettelkasten/SKILL.md) — Successor

Frequently asked questions