Lean applied reasoning
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-applied-reasoningAssembled 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: Applied reasoning for intelligence analysis, strategy creation and analysis, brainstorming methodologies, investigative reasoning, and domain-specific decision-making. Use when formalizing strategic frameworks, situational analysis, hypothesis generation workflows, decision-under-uncertainty models, or when connecting theoretical formalization to practical operational contexts. Bridges mathematical formalization to real-world application domains. DO NOT USE FOR: pure intelligence-analysis methodology (use @applied-intelligence-analysis); strategy analysis methodology (use @applied-strategy-analysis); legal reasoning methodology (use @applied-legal-reasoning). TRIGGERS: applied reasoning, intelligence formalisation, strategy formalisation, investigative reasoning, domain-specific reasoning.
SKILL.md
4.1 KB, as published. Nobody here has run it
Lean 4 Applied Reasoning & Strategy
Guide to formalizing applied reasoning — from intelligence analysis to strategic decision-making — in Lean 4.
Routing
- USE FOR: Applied reasoning for intelligence analysis, strategy creation and analysis, brainstorming methodologies, investigative reasoning, and domain-specific decision-making. Use when formalizing strategic frameworks, situational analysis, hypothesis generation workflows, decision-under-uncertainty models, or when connecting theoretical formalization to practical operational contexts. Bridges mathematical formalization to real-world application domains.
- DO NOT USE FOR: pure intelligence-analysis methodology (use @applied-intelligence-analysis); strategy analysis methodology (use @applied-strategy-analysis); legal reasoning methodology (use @applied-legal-reasoning).
- TRIGGERS: applied reasoning, intelligence formalisation, strategy formalisation, investigative reasoning, domain-specific reasoning.
Workflow
- Classify the applied-reasoning task: intelligence-formalisation, strategy-formalisation, investigative-reasoning, or domain-specific reasoning.
- Pick the corresponding body section; identify the Lean primitives + Mathlib lemmas it depends on.
- Write the Lean encoding; verify Mathlib primitives exist at the current pin.
- Hand off: to
@lean-proof-reviewfor review, to@lean-enforcementfor CI, to@lean-zettelkasten.
Recovery & STOP
- STOP if the question is purely methodological (no Lean) — delegate to the matching applied-* skill.
- STOP if Mathlib primitives are missing — escalate to
@lean-research. - STOP if the spec is informal — delegate to
@lean-specificationfirst.
Handoffs
- Predecessors:
agent:gateway,skill:lean-research. - Successors:
skill:lean-proof-review,skill:lean-enforcement,skill:lean-zettelkasten.
Detailed reference
Full content for lean-applied-reasoning lives in
references/lean-applied-reasoning-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 | Intelligence Analysis Formalization |
| Part 2 | Strategy Formalization |
| Part 3 | Brainstorming Methodology |
| Part 4 | Investigative Reasoning (Project Core Domain) |
| Part 5 | Decision Under Uncertainty |
| Part 6 | Project & Product Management for Mathematics |
| Part 7 | Research Council Integration |
See also
../../references/lean-applied-reasoning-handbook.md— Full handbook (extracted from this skill)../lean-proof-review/SKILL.md— Successor../lean-enforcement/SKILL.md— Successor../lean-zettelkasten/SKILL.md— Successor