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.

1.13x

Quality

92%

Does it follow best practices?

Impact

93%

1.13x

Average score across 3 eval scenarios

Securityby

Passed

No known issues

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%

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%

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%

Repository: ArabelaTso/Skills-4-SE
Commit: 0f00a4f

Evaluated: 29 days ago
Agent: Claude Code
Model: Claude Sonnet 4.6

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.