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

83%

Does it follow best practices?

Impact

93%

1.13x

Average score across 3 eval scenarios

Securityby

Passed

No findings from the security scan

Preview

This is a new way to view eval results. We're still working on it, so the layout may change.

Run	Type	Date	Status
baseline vs usage-spec With / without context 7 months ago Completed	With / without context	7 months ago	Completed

Eval run

019cc49d-f616-778c-84ec-6f637406d1d8

Run 7 months ago

Stats are not available yet

The run is available. Its result stats will appear here when they are ready.

Repository: ArabelaTso/Skills-4-SE
Path: skills/lemma-discovery-assistant/SKILL.md
Commit: 4f38503

Evaluated: 7 months 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.