Lean knowledge formalization
Skill r-irbe/proof-skills/skills/lean-knowledge-formalization
USE FOR: Knowledge representation, ontology engineering, symbolic AI, commonsense reasoning, causal reasoning, legal reasoning, and abductive inference in Lean 4. Use when formalizing knowledge structures, reasoning systems, argumentation frameworks, deontic logic, defeasible reasoning, or any domain where structured knowledge and inference must be formally verified. Core skill for knowledge-lifecycle and provenance architectures. DO NOT USE FOR: KRR methodology not in Lean (use @ai-symbolic-neuro); commonsense reasoning methodology (use @ai-commonsense-reasoning); causal/deontic methodology (use @ai-causal-deontic). TRIGGERS: knowledge formalisation, ontology in Lean, symbolic AI Lean, abductive inference Lean, legal reasoning Lean.From its SKILL.md
npx -y skills add r-irbe/proof-skills --skill lean-knowledge-formalizationAssembled 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.
SKILL.md
4.0 KB, 717 tokens by cl100k_base, as published. Nobody here has run it
Lean 4 Knowledge Systems & Reasoning Formalization
Guide to formalizing knowledge representation, reasoning systems, and domain-specific logic in Lean 4.
Routing
- USE FOR: Knowledge representation, ontology engineering, symbolic AI, commonsense reasoning, causal reasoning, legal reasoning, and abductive inference in Lean 4. Use when formalizing knowledge structures, reasoning systems, argumentation frameworks, deontic logic, defeasible reasoning, or any domain where structured knowledge and inference must be formally verified. Core skill for knowledge-lifecycle and provenance architectures.
- DO NOT USE FOR: KRR methodology not in Lean (use @ai-symbolic-neuro); commonsense reasoning methodology (use @ai-commonsense-reasoning); causal/deontic methodology (use @ai-causal-deontic).
- TRIGGERS: knowledge formalisation, ontology in Lean, symbolic AI Lean, abductive inference Lean, legal reasoning Lean.
Workflow
- Classify the knowledge object: ontology, taxonomy, causal model, deontic norm, or abductive rule.
- Pick the matching encoding pattern from the body (description-logic encoding, SCM encoding, etc.).
- Produce the Lean encoding; check Mathlib primitives at the current pin.
- Hand off: to
@lean-causal-reasoningif causal-DAG-specific, to@lean-proof-reviewfor review, to@lean-zettelkasten.
Recovery & STOP
- STOP if the question is methodological (not Lean) — delegate to
@ai-symbolic-neuro/@ai-commonsense-reasoning/@ai-causal-deontic. - STOP if Mathlib lacks the needed structure — escalate to
@lean-research. - STOP if the encoding requires graph-theoretic foundations not in the body — delegate to
@lean-math-discreteor@math-graph-knowledge.
Handoffs
- Predecessors:
agent:gateway,skill:lean-research. - Successors:
skill:lean-proof-review,skill:lean-causal-reasoning,skill:lean-zettelkasten.
Detailed reference
Full content for lean-knowledge-formalization lives in
references/lean-knowledge-formalization-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 | Knowledge Representation |
| Part 2 | Reasoning Systems |
| Part 3 | Legal Reasoning |
| Part 4 | Symbolic AI |
| Part 5 | Intelligence Analysis Reasoning |
| Part 6 | Research Council Integration |
See also
../../references/lean-knowledge-formalization-handbook.md— Full handbook (extracted from this skill)../lean-proof-review/SKILL.md— Successor../lean-causal-reasoning/SKILL.md— Successor../lean-zettelkasten/SKILL.md— Successor
What ships with it
Read from the repository
Just SKILL.md. No reference files, no scripts.