Lean doc requirements
APM-installable agent skills for Lean 4 and Mathlib4 — proof tactics, math domains, review and research workflows, generic tooling.
npx -y skills add r-irbe/proof-skills --skill lean-doc-requirementsAssembled 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: 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.md
3.7 KB, as published. Nobody here has run it
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
- Read the source document; identify each informal mathematical claim, its scope, and implicit assumptions.
- Pick the requirement template from the body matching the claim class (definition, theorem, lemma, tactic-rule).
- Produce a draft Lean specification (signature only, no proof) with traceability back to the source.
- Hand off: to
@lean-specificationfor the formal spec design, to@lean-prooffor 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.
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— Full handbook (extracted from this skill)../lean-specification/SKILL.md— Successor../_overrides/lean-proof/SKILL.md— Successor../lean-zettelkasten/SKILL.md— Successor