proof-skeleton-generator
Generate structured proof skeletons with tactics, strategies, and intermediate lemmas for theorems in Isabelle/HOL or Coq. Use when users need to: (1) Create proof outlines for theorem statements, (2) Generate proof structure with tactic placeholders, (3) Identify key lemmas needed for a proof, (4) Plan proof strategies (induction, case analysis, forward/backward reasoning), (5) Scaffold proofs with intermediate steps and subgoals, or (6) Convert theorem statements into detailed proof templates. Supports both Isabelle/HOL and Coq equally.
npx skills add majiayu000/claude-skill-registry --skill proof-skeleton-generator --agent claude-code
Same command for any agent — swap --agent for codex, cursor, copilot.
Weekly change comes from our own snapshots, not the repository page — it measures attention, not adoption.
# Proof Skeleton Generator Generate structured proof skeletons with tactics, proof strategies, and key lemmas for theorems in Isabelle/HOL or Coq. ## Workflow ### 1. Analyze the Theorem Statement Examine the theorem to understand: - **Quantifiers**: Universal (∀/forall) or existential (∃/exists) - **Logical structure**: Implications, conjunctions, disjunctions - **Data types involved**: Lists, natural numbers, custom types - **Complexity**: Simple equality vs. complex property ### 2. Choose Target System Ask the user which proof assistant to target: - **Isabelle/HOL**: Uses Isar structured proofs, automatic tactics - **Coq**: Uses Ltac tactics, more explicit proof terms - **Both**: Generate skeletons for both systems If not specified, default to generating both versions. ### 3. Determine Proof Strategy Based on the theorem structure, identify the appropriate proof technique: **Induction** - When theorem involves recursive types: - List induction for list properties - Natural number induction for arithmetic - Structural induction for custom datatypes - Strong induction when needed **Case Analysis** - When theorem involves: - Boolean conditions - Option types (None/Some) - Sum types
- Workflow
- 1. Analyze the Theorem Statement
- 2. Choose Target System
- 3. Determine Proof Strategy
- 4. Identify Required Lemmas
- 5. Generate Proof Skeleton
- 6. Structure the Output
- Key Principles
- Clarity
- Completeness
- Practicality
- Correctness
- Proof Strategy Selection Guide
- When to Use Induction
What does the proof-skeleton-generator skill do?
Generate structured proof skeletons with tactics, strategies, and intermediate lemmas for theorems in Isabelle/HOL or Coq. Use when users need to: (1) Create proof outlines for theorem statements, (2) Generate proof structure with tactic placeholders, (3) Identify key lemmas needed for a proof, (4) Plan proof strategies (induction, case analysis, forward/backward reasoning), (5) Scaffold proofs with intermediate steps and subgoals, or (6) Convert theorem statements into detailed proof templates. Supports both Isabelle/HOL and Coq equally.
How do I install it?
Run `npx skills add majiayu000/claude-skill-registry --skill proof-skeleton-generator --agent claude-code` — it drops the skill into your project so the agent can pick it up. Swap the --agent value for codex, cursor or copilot if you use one of those.
Where does this skill come from?
From majiayu000/claude-skill-registry, a repository with 534 stars. We read it straight from the repository tree rather than a submitted listing, so what you see here is what is actually published.
Is a popular skill a good skill?
Not necessarily. Stars measure attention, not adoption — a repository can trend for a week and be abandoned. That is why we show the weekly change from our own snapshots next to the total, instead of a single flattering number.