lemma-discovery-assistant

Analyze failed or stuck proofs and propose auxiliary lemmas to help complete the proof in Isabelle/HOL or Coq. Use when encountering proof failures, stuck proof states, unprovable subgoals, or when needing to strengthen induction hypotheses. Identifies missing lemmas, suggests proof strategies, and generates helper lemmas with appropriate statements and proof sketches. Supports inductive proofs, case analysis, rewriting, and complex proof obligations.

Install with Tessl CLI

npx tessl i github:ArabelaTso/Skills-4-SE --skill lemma-discovery-assistant

What are skills?

Review — 92%

Does it follow best practices?

Validation — 11 / 11 Passed

Validation for skill structure

SKILL.md

Review

Evals

Evaluation results

100%

22%

BST Insert Correctness: Stuck Isabelle Proof

Structured Isabelle lemma discovery process

Criteria

Without context

With context

Gap type labeled

30%

100%

Proof state analysis

70%

100%

Isabelle lemma syntax

100%

set_tree insert lemma

100%

Proof strategy per lemma

100%

Usage explanation

80%

100%

Non-circular lemmas

100%

Lemma search tools mentioned

100%

General lemma formulation

100%

Descriptive lemma names

100%

Without context: $0.2719 · 1m 55s · 10 turns · 15 in / 6,297 out tokens

With context: $0.9263 · 3m 43s · 24 turns · 5,763 in / 11,914 out tokens

100%

Tail-Recursive Reverse: Stuck Coq Proof

Coq induction strengthening and modern tactics

Criteria

Without context

With context

Induction gap identified

100%

Gap type classified

60%

100%

Generalized lemma proposed

100%

Coq lemma syntax correct

100%

Non-circular

100%

Search not SearchAbout

70%

100%

lia not omega

100%

Proof strategy for generalized lemma

100%

Usage in original theorem

100%

Descriptive lemma name

100%

Without context: $0.3309 · 2m 15s · 10 turns · 13 in / 7,122 out tokens

With context: $0.4903 · 2m 24s · 18 turns · 54 in / 5,723 out tokens

80%

Tree Mirror and In-Order Traversal: Multi-Gap Isabelle Proof

Bottom-up multi-lemma discovery and troubleshooting

Criteria

Without context

With context

Named discovery strategy

60%

At least two lemmas

100%

Gap type per obstacle

50%

rev_append lemma

100%

Isabelle lemma syntax

100%

Proof strategy per lemma

100%

Troubleshooting analysis

40%

50%

Non-circularity addressed

70%

100%

Usage chain explained

100%

Descriptive lemma names

100%

Without context: $0.3268 · 2m 22s · 12 turns · 17 in / 7,464 out tokens

With context: $1.1429 · 5m 18s · 26 turns · 5,522 in / 17,858 out tokens

Evaluated: about 12 hours ago
Agent: Claude Code

Table of Contents

BST Insert Correctness: Stuck Isabelle Proof Tail-Recursive Reverse: Stuck Coq Proof Tree Mirror and In-Order Traversal: Multi-Gap Isabelle Proof

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.