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.

Install with Tessl CLI

npx tessl i github:ArabelaTso/Skills-4-SE --skill proof-skeleton-generator

What are skills?

Review — 85%

Does it follow best practices?

If you maintain this skill, you can automatically optimize it using the tessl CLI to improve its score:

npx tessl skill review --optimize ./path/to/skill

Learn more

Validation — 11 / 11 Passed

Validation for skill structure

SKILL.md

Review

Evals

Evaluation results

80%

-15%

Proof Skeleton: List Map Composition

Dual-system list proof skeleton

Criteria

Without context

With context

Isabelle skeleton present

100%

Coq skeleton present

100%

Isabelle list induction method

100%

Isabelle induction case labels

100%

Coq list induction as-pattern

100%

Coq case bullet notation

100%

Isabelle uses sorry

100%

Coq uses admit/Admitted

50%

IH documentation

100%

Strategy comments

100%

Helper lemma included

100%

Automation tactic suggestion

100%

Without context: $0.1632 · 1m 1s · 9 turns · 14 in / 3,423 out tokens

With context: $0.7333 · 2m 49s · 23 turns · 10,685 in / 8,424 out tokens

98%

28%

Proof Skeleton: Fibonacci Bounds in Coq

Coq natural number induction skeleton

Criteria

Without context

With context

Coq Proof./Admitted. structure

100%

intros at start

100%

Named induction hypothesis

100%

admit for incomplete steps

100%

Admitted. not Qed.

100%

lia not omega

100%

IH comment documentation

100%

Strategy comments per case

100%

Bullet notation for cases

50%

75%

Helper lemma skeleton

100%

Without context: $0.9800 · 6m 20s · 11 turns · 16 in / 26,034 out tokens

With context: $0.9547 · 5m 29s · 23 turns · 108 in / 18,294 out tokens

100%

43%

Proof Skeleton: Safe Division with Option Types in Isabelle

Isabelle case analysis skeleton

Criteria

Without context

With context

Isar proof/qed structure

100%

Cases invocation

30%

100%

Exhaustive cases

20%

100%

show ?thesis or show ?case

80%

100%

sorry placeholders

100%

Goal comments

100%

Strategy comments

100%

sledgehammer suggestion

100%

Automation tactic noted

100%

Assumptions referenced

100%

Without context: $0.1573 · 50s · 10 turns · 15 in / 2,693 out tokens

With context: $0.4875 · 2m 11s · 15 turns · 2,244 in / 6,986 out tokens

Evaluated: about 20 hours ago
Agent: Claude Code

Table of Contents

Proof Skeleton: List Map Composition Proof Skeleton: Fibonacci Bounds in Coq Proof Skeleton: Safe Division with Option Types in Isabelle

Is this your skill?

If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.