Math strategy studio
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 math-strategy-studioAssembled 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: Strategic mathematical thinking — brainstorming, problem decomposition, proof strategy design, creative hypothesis generation, and mathematical intuition development. Use when facing novel formalization challenges, when standard approaches fail, when exploring connections between domains, or when the theorem specification needs creative mathematical insight. The creative counterpart to the systematic research-council and review-council skills. DO NOT USE FOR: strategy analysis methodology generally (use @applied-strategy-analysis); research synthesis (use @research-synthesis-engine); Lean specification (use @lean-specification). TRIGGERS: strategy studio, brainstorming, problem decomposition, proof strategy, creative hypothesis, mathematical intuition.
SKILL.md
4.0 KB, 646 tokens by cl100k_base, as published. Nobody here has run it
Mathematical Strategy Studio
Creative mathematical thinking and proof strategy design for Lean 4 formalization.
Routing
- USE FOR: Strategic mathematical thinking — brainstorming, problem decomposition, proof strategy design, creative hypothesis generation, and mathematical intuition development. Use when facing novel formalization challenges, when standard approaches fail, when exploring connections between domains, or when the theorem specification needs creative mathematical insight. The creative counterpart to the systematic research-council and review-council skills.
- DO NOT USE FOR: strategy analysis methodology generally (use @applied-strategy-analysis); research synthesis (use @research-synthesis-engine); Lean specification (use @lean-specification).
- TRIGGERS: strategy studio, brainstorming, problem decomposition, proof strategy, creative hypothesis, mathematical intuition.
Workflow
- Frame the strategy question: brainstorming, problem decomposition, proof-strategy design, hypothesis generation, or intuition-building.
- Pick the matching method from the body; surface 3-5 candidate strategies for evaluation.
- Score the candidates; recommend the top strategy with explicit assumptions and fallbacks.
- Hand off: to
@lean-specificationfor proof-strategy execution, to@research-councilfor hypothesis vetting, to@lean-zettelkasten.
Recovery & STOP
- STOP if the question is applied-strategy (not mathematical) — delegate to
@applied-strategy-analysis. - STOP if no candidate scores above the belief floor — escalate to
@research-council. - STOP if the question is about synthesising prior work — delegate to
@research-synthesis-engine.
Handoffs
- Predecessors:
agent:gateway,skill:lean-research. - Successors:
skill:lean-specification,skill:research-council,skill:lean-zettelkasten.
Detailed reference
Full content for math-strategy-studio lives in
references/math-strategy-studio-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 | Strategy Design Framework |
| Part 2 | Proof Strategy Patterns |
| Part 3 | Creative Techniques |
| Part 4 | Brainstorming Protocols |
| Part 5 | Problem Decomposition for Complex Theorems |
| Part 6 | Mathematical Intuition Development |
| Part 7 | Research Council Integration |
See also
../../references/math-strategy-studio-handbook.md— Full handbook (extracted from this skill)../lean-specification/SKILL.md— Successor../research-council/SKILL.md— Successor../lean-zettelkasten/SKILL.md— Successor