New: 98,000+ skills indexed from GitHub repos with 100+ stars · every skill safety-checkedBrowse top skillsTop skills
Esc to closeBrowse all skills
Submit a skillBrowse skills
Submit a skillBrowse skills

Agent skill

Proof Skeleton Generator

by ArabelaTso in ArabelaTso/Skills-4-SE

Generate structured proof skeletons with tactics, strategies, and intermediate lemmas for theorems in Isabelle/HOL or Coq.

Apache-2.0Auto-check passed

Install Proof Skeleton Generator

skills CLI
$ npx skills add ArabelaTso/Skills-4-SE --skill proof-skeleton-generator -a claude-code

Project install by default; add -g for ~/.claude/skills/.

GitHub CLI
$ gh skill install ArabelaTso/Skills-4-SE proof-skeleton-generator --agent claude-code

Project scope by default; add --scope user for a personal install. Needs GitHub CLI 2.90.0 or later (public preview).

Manual copy
$ git clone --depth 1 https://github.com/ArabelaTso/Skills-4-SE.git skills-src && mkdir -p .claude/skills && cp -r skills-src/skills/proof-skeleton-generator .claude/skills/proof-skeleton-generator && rm -rf skills-src

Use ~/.claude/skills/ instead of .claude/skills for a personal install. The folder must contain SKILL.md.

Claude Code skills documentation · loads skills from .claude/skills/

Facts

Skill name
proof-skeleton-generator
GitHub stars
253
Token cost
~1.8k tokens
SKILL.md length
687 words
Files
4 (incl. references)
Skills in repo
170
Repo updated
First seen
Licence
Apache-2.0

At a glance

Generate structured proof skeletons with tactics, strategies, and intermediate lemmas for theorems in Isabelle/HOL or Coq.

  • Works in 6 steps: Analyze the Theorem Statement → Choose Target System → Determine Proof Strategy → …
  • Create proof outlines for theorem statements
  • SKILL.md covers Workflow, Key Principles, Proof Strategy Selection Guide and Common Patterns, plus 1 more section
  • Instructions only: no scripts, shell commands, URLs or credentials in SKILL.md

What it does

Proof Skeleton Generator is an agent skill from ArabelaTso/Skills-4-SE. 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…

Its SKILL.md is about 1.8k tokens, which your agent loads only when the skill is triggered. The skill folder holds 4 other files, including reference files (for example `references/coq_tactics.md`, `references/examples.md` and `references/isabelle_tactics.md`).

The repository describes itself as: A curated list of 180+ useful Claude Skills for Software Engineering and resources for customizing AI for SE workflows. The licence is Apache-2.0.

When your agent uses it

  • Create proof outlines for theorem statements
  • Generate proof structure with tactic placeholders
  • Identify key lemmas needed for a proof
  • Plan proof strategies (induction

Example prompts

  • “/proof-skeleton-generator”

Workflow steps

6 steps, taken from the step headings in SKILL.md.

  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

What it can do on your machine

Read from SKILL.md and the folder at commit 4f38503. It shows what the files ask for, not the result of running them.

  • Tool permissions

    Pre-approves nothing: there is no allowed-tools line, so your agent's usual permission prompts apply.

    From allowed-tools in the SKILL.md frontmatter.

  • Runs code

    No scripts in the folder and no shell commands in SKILL.md (its code samples are isabelle and coq).

    From the folder's file list and the shell code blocks in SKILL.md.

  • Network

    No URLs in SKILL.md.

    From URLs in SKILL.md, links to its own repository left out.

  • Credentials

    Names no API keys, tokens, secrets or passwords.

    From names ending in _API_KEY, _TOKEN, _SECRET, _KEY or _PASSWORD in SKILL.md.

Context cost

Proof Skeleton Generator loads about 1.8k tokens when it runs, and up to ~6.7k if it reads all its reference files. Until then it costs about 142 tokens; SKILL.md has 687 words of instructions outside code blocks.

Always · name and description, kept in context so the agent knows when to use it
~142
When it runs · the whole SKILL.md, loaded when a task matches
~1.8k
With references · SKILL.md plus every file in references/, read only if the agent opens them
~6.7k

Estimates: characters ÷ 4, the usual rule of thumb; real counts depend on the model's tokenizer. Scripts and assets cost tokens only if the agent reads them.

Safety

Auto-check passed

The automated check found no risky patterns in SKILL.md.

Automated static check — not a guarantee. Review scripts before installing. It scans the text of SKILL.md for risky patterns (piping downloads into a shell, reading credential files, hidden Unicode, destructive commands); files beside SKILL.md are not scanned.

SKILL.md

The full file from ArabelaTso/Skills-4-SE at commit 4f38503, republished under its Apache-2.0 licence (© ArabelaTso). 687 words, ~1,816 tokens.

Download SKILL.mdSave it as .claude/skills/proof-skeleton-generator/SKILL.md (or your agent's skills folder). This skill also uses 3 other files; get the full folder from GitHub.
name
proof-skeleton-generator
description
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.

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 or custom constructors
  • Conditional expressions

Direct Proof - When theorem is:

  • Simple equality that simplifies
  • Follows directly from definitions
  • Provable by automatic tactics

Forward Reasoning - Build up facts:

  • Establish intermediate lemmas
  • Chain implications
  • Construct witnesses for existentials

Backward Reasoning - Work from goal:

  • Apply rules to reduce goal
  • Split conjunctions
  • Introduce implications
4. Identify Required Lemmas

Determine helper lemmas that may be needed:

  • Standard library lemmas: Check if already available
  • Custom lemmas: Properties that need separate proof
  • Induction hypotheses: How they'll be used
  • Intermediate facts: Steps in the main proof
5. Generate Proof Skeleton

Use the reference files for tactics and patterns:

Create a skeleton that includes:

  1. Proof structure with appropriate method (induction, cases, etc.)
  2. Case labels for each subgoal
  3. Strategy comments explaining the approach
  4. Tactic placeholders (sorry/admit) for incomplete steps
  5. Intermediate assertions (have/assert) for key facts
  6. Helper lemmas with their own skeletons
6. Structure the Output

Organize the proof skeleton clearly:

For Isabelle/HOL:

isabelle
(* Helper lemmas if needed *)
lemma helper_name:
  "statement"
  sorry

(* Main theorem *)
theorem theorem_name:
  assumes "assumptions"
  shows "conclusion"
proof (method)
  case case_name
  (* Goal: ... *)
  (* Strategy: ... *)
  (* Key steps:
     1. ...
     2. ...
  *)
  show ?case sorry
next
  (* Additional cases *)
qed

For Coq:

coq
(* Helper lemmas if needed *)
Lemma helper_name :
  statement.
Proof.
  (* proof *)
  admit.
Admitted.

(* Main theorem *)
Theorem theorem_name :
  statement.
Proof.
  intros.
  induction ... as [| ...].
  - (* Case: ... *)
    (* Strategy: ... *)
    admit.
  - (* Case: ... *)
    (* IH: ... *)
    (* Strategy: ... *)
    admit.
Admitted.

Key Principles

Clarity
  • Add comments explaining the proof strategy
  • Label each case clearly
  • Document what the induction hypothesis provides
  • Explain non-obvious steps
Completeness
  • Include all necessary cases
  • Identify all required helper lemmas
  • Show the structure of nested proofs
  • Indicate where automation might work
Practicality
  • Use sorry (Isabelle) or admit (Coq) for incomplete steps
  • Suggest automatic tactics where applicable
  • Note when sledgehammer (Isabelle) might help
  • Indicate which steps are trivial vs. challenging
Correctness
  • Ensure case analysis is exhaustive
  • Verify induction is on the right variable
  • Check that the proof structure matches the goal
  • Validate that lemmas are actually needed
Show full SKILL.md (269 more words)Show less

Proof Strategy Selection Guide

When to Use Induction

List properties: forall xs, P xs

  • Induction on xs
  • Base case: empty list
  • Inductive case: x :: xs with IH P xs

Natural number properties: forall n, P n

  • Induction on n
  • Base case: 0 or Suc 0
  • Inductive case: Suc n with IH P n

Recursive function properties: When function is defined recursively

  • Induct on the recursive argument
  • IH mirrors the recursive call
When to Use Case Analysis

Conditional expressions: if b then ... else ...

  • Split on b (true/false cases)

Option types: match opt with None => ... | Some x => ...

  • Case on None and Some x

Sum types: match x with Left a => ... | Right b => ...

  • Case on each constructor
When to Use Direct Proof

Definitional equalities: f x = g x where definitions unfold

  • Unfold definitions and simplify

Trivial goals: Provable by auto, simp, reflexivity

  • Try automatic tactics first
When to Use Lemmas

Repeated subgoals: Same property needed multiple times

  • Extract as separate lemma

Complex intermediate facts: Multi-step derivations

  • Prove as helper lemma

Standard properties: Check standard library first

  • Import and use existing lemmas

Common Patterns

Induction with Simplification
proof (induction xs)
  case Nil
  show ?case by simp
next
  case (Cons x xs)
  show ?case using Cons.IH by simp
qed
Case Analysis with Subproofs
proof (cases x)
  case Constructor1
  show ?thesis
  proof -
    (* detailed steps *)
  qed
next
  case Constructor2
  (* ... *)
qed
Forward Reasoning Chain
proof -
  have step1: "fact1" by simp
  have step2: "fact2" using step1 by simp
  show ?thesis using step2 by simp
qed
Backward Reasoning with Rules
proof (rule some_rule)
  show "premise1" sorry
  show "premise2" sorry
qed

Tips

  • Start with structure: Get the proof skeleton right before filling details
  • Use comments liberally: Explain strategy and key steps
  • Identify IH usage: Note where induction hypothesis is applied
  • Check standard library: Many lemmas already exist
  • Suggest automation: Note where auto, simp, blast might work
  • Be realistic: Mark challenging steps as sorry/admit
  • Both systems: Ensure semantic equivalence when generating both
  • Nested induction: Handle carefully with clear variable names
  • Termination: Note when termination proofs are needed

© ArabelaTso, Apache-2.0. Rendered from Markdown: HTML in the file is shown as text, images as links, and headings moved down two levels. Raw file

Files

SKILL.md and 3 other files (references) in skills/proof-skeleton-generator of ArabelaTso/Skills-4-SE.

  • SKILL.md
  • references/coq_tactics.md
  • references/examples.md
  • references/isabelle_tactics.md

Open the folder on GitHubat commit 4f38503

Compare with similar skills

Proof Skeleton Generator next to the 5 skills that share the most tags, products or categories with it. Stars are the repository's; “used in” counts other GitHub owners with a copy.

Proof Skeleton Generator compared with similar skills
SkillStarsUsed inTokensAuto-checkLicenceRepo updated
Proof Skeleton Generator this skillArabelaTso/Skills-4-SE253—~1.8kAutomated safety check: PassApache-2.0
Trading Strategy GeneratorHKUDS/Vibe-Trading35k—~4.2kAutomated safety check: PassMIT
Proof Strategyjeremylongshore/tons-of-skills-marketplace2.8k—~1.5kAutomated safety check: NotesMIT
Generatealirezarezvani/claude-skills28k1 repos~1.1kAutomated safety check: PassMIT
Free Tool Strategyalirezarezvani/claude-skills28k—~3.1kAutomated safety check: PassMIT
Fal Generatenexu-io/open-design100k—~306Automated safety check: PassApache-2.0

Similar skills

  • Trading Strategy Generator

    HKUDS/Vibe-Trading

    Takes a trading idea from request to backtest: pins down instruments and dates, writes config.json and a signal engine, runs the backtest and iterates on the metrics.

    35k GitHub stars~4.2k tokensUpdated yesterday
    Business, Finance & HRAuto-check passed

  • Proof Strategy

    jeremylongshore/tons-of-skills-marketplace

    Produce a test strategy for a project or feature — risk map, test type decisions, coverage targets, CI config.

    2.8k GitHub stars~1.5k tokensUpdated yesterday
    Testing & QAAuto-check: notes

  • Generate

    alirezarezvani/claude-skills

    Generate Playwright tests. An agent skill from alirezarezvani/claude-skills.

    28k GitHub starsUsed in 1 repo~1.1k tokens
    Testing & QAAuto-check passed

  • Free Tool Strategy

    alirezarezvani/claude-skills

    When the user wants to build a free tool for marketing — lead generation, SEO value, or brand awareness.

    28k GitHub stars~3.1k tokensUpdated 1 mo ago
    Marketing & SEOAuto-check passed

  • Fal Generate

    nexu-io/open-design

    Generate images and videos using fal.ai AI models. An agent skill from nexu-io/open-design.

    100k GitHub stars~306 tokensUpdated yesterday
    Media & CreativeAuto-check passed

  • Good Strategy Bad Strategy

    wondelai/skills

    Formulate and audit real strategy using Richard Rumelt's "Good Strategy Bad Strategy": an honest diagnosis, a guiding policy, and coherent action instead of goals, vision, and wishful thinking.

    2.4k GitHub stars~4.8k tokensUpdated 1 mo ago
    Business, Finance & HRAuto-check passed

More from ArabelaTso/Skills-4-SE

All 170 skills in this repo

  • Framework Migration Assistant

    ArabelaTso/Skills-4-SE

    Automatically migrate Python web applications between frameworks (Flask → FastAPI, Django → FastAPI).

    253 GitHub stars~1.9k tokensUpdated 1 mo ago
    Auto-check passed

  • Metamorphic Test Generator

    ArabelaTso/Skills-4-SE

    Generate test cases using metamorphic testing by applying transformations based on metamorphic properties.

    253 GitHub stars~798 tokensUpdated 1 mo ago
    Auto-check passed

  • Reproduction Trace Instrumenter

    ArabelaTso/Skills-4-SE

    Instruments programs to capture execution traces specifically for reproducing reported bugs, enabling consistent replay and diagnosis of failures.

    253 GitHub stars~2.4k tokensUpdated 1 mo ago
    Auto-check passed

  • Spring Mvc To Boot Migrator

    ArabelaTso/Skills-4-SE

    Automatically migrate Spring MVC applications to Spring Boot.

    253 GitHub stars~2.2k tokensUpdated 1 mo ago
    Auto-check passed

  • State Snapshot Instrumenter

    ArabelaTso/Skills-4-SE

    Instrument programs (Python, C/C++, Java) to capture snapshots of key program states at runtime, including variables, memory, and call stacks.

    253 GitHub stars~2.2k tokensUpdated 1 mo ago
    Auto-check passed

Questions about Proof Skeleton Generator

What does Proof Skeleton Generator do?

Generate structured proof skeletons with tactics, strategies, and intermediate lemmas for theorems in Isabelle/HOL or Coq. Proof Skeleton Generator is an agent skill from ArabelaTso/Skills-4-SE. Generate structured proof skeletons with tactics, strategies, and intermediate lemmas for theorems in Isabelle/HOL or Coq.

When should I use Proof Skeleton Generator?

Proof Skeleton Generator fits situations like: create proof outlines for theorem statements; generate proof structure with tactic placeholders; identify key lemmas needed for a proof; plan proof strategies (induction.

How do I install Proof Skeleton Generator in Claude Code?

Run `npx skills add ArabelaTso/Skills-4-SE --skill proof-skeleton-generator -a claude-code`. Or copy the skill folder (skills/proof-skeleton-generator in ArabelaTso/Skills-4-SE) into .claude/skills/proof-skeleton-generator in your project. Claude Code loads it when a task matches its description.

How do I install Proof Skeleton Generator in Codex?

Run `npx skills add ArabelaTso/Skills-4-SE --skill proof-skeleton-generator -a codex`. Or copy the skill folder (skills/proof-skeleton-generator in ArabelaTso/Skills-4-SE) into .agents/skills/proof-skeleton-generator in your project. Codex loads it when a task matches its description.

Can I use Proof Skeleton Generator in Cursor, Gemini CLI or GitHub Copilot?

Cursor, Gemini CLI, GitHub Copilot and OpenCode also load SKILL.md folders. With the skills CLI, run `npx skills add ArabelaTso/Skills-4-SE --skill proof-skeleton-generator -a cursor` (or -a gemini-cli, github-copilot or opencode for the others). To copy it by hand, put the folder in .cursor/skills/proof-skeleton-generator, .gemini/skills/proof-skeleton-generator, .github/skills/proof-skeleton-generator and .opencode/skills/proof-skeleton-generator in your project.

What does Proof Skeleton Generator need to run?

SKILL.md names no scripts, command-line tools or credentials: Proof Skeleton Generator is instructions for the agent only.

Does Proof Skeleton Generator access the network?

SKILL.md contains no URLs. Any network use would come from the scripts or tools the agent runs. This is read from the text; nothing was executed.

Is Proof Skeleton Generator safe to install?

Our automated static check of SKILL.md found no risky patterns, such as piping downloads into a shell, reading credential files or hidden Unicode. It is not a guarantee. Review the folder before installing.

What licence does Proof Skeleton Generator use?

Proof Skeleton Generator is published under the Apache-2.0 licence (the repository's licence). It allows redistribution, so the full SKILL.md is shown on this page.

How many tokens does Proof Skeleton Generator use?

About 1.8k tokens (SKILL.md is roughly 7.3k characters). Agents keep only the skill's name and description in context until a task matches; then they load SKILL.md in full. Its references folder adds about 4.9k tokens, read only when the agent opens those files.

What are the alternatives to Proof Skeleton Generator?

Skills that share tags, products or a category with Proof Skeleton Generator: Trading Strategy Generator (HKUDS/Vibe-Trading, 35k stars), Proof Strategy (jeremylongshore/tons-of-skills-marketplace, 2.8k stars), Generate (alirezarezvani/claude-skills, 28k stars) and Free Tool Strategy (alirezarezvani/claude-skills, 28k stars). The comparison table on this page puts their stars, adoption, token cost, safety result and licence side by side.

Who maintains Proof Skeleton Generator?

ArabelaTso (a GitHub user) maintains it in ArabelaTso/Skills-4-SE, which has 253 GitHub stars. The repository holds 170 skills in this directory. The repository was last updated on August 21, 2026.

Source: ArabelaTso/Skills-4-SE on GitHub. Facts on this page come from the repository at the commit we read; the author's words are quoted as theirs.