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

Quality

Content

85%

Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.

This is a well-structured skill with excellent actionability and workflow clarity, providing concrete executable examples in both Isabelle and Coq. The progressive disclosure is appropriate with clear references to supplementary materials. However, the content could be more concise by removing explanatory sections about concepts Claude already understands (like what makes proofs get stuck) and trimming the descriptive lists.

Suggestions

Remove or significantly condense the 'Common Symptoms' and 'Questions to ask' sections - Claude understands these concepts and they add ~30 lines of low-value content

Trim the 'Lemma characteristics' and 'Gap types' bullet lists to inline mentions within the examples rather than standalone sections

Dimension	Reasoning	Score
Conciseness	The skill contains useful content but is verbose in places, with explanatory sections like 'When Proofs Get Stuck' and 'Common Symptoms' that describe concepts Claude likely already understands. The 'Questions to ask' and 'Lemma characteristics' lists add padding without adding actionable value.	2 / 3
Actionability	The skill provides fully executable code examples in both Isabelle and Coq, showing complete proof scripts with specific tactics. The examples demonstrate stuck proofs, proposed lemmas, and how to apply them - all copy-paste ready.	3 / 3
Workflow Clarity	The 5-step lemma discovery process is clearly sequenced (Analyze → Identify Gap → Propose → Suggest Strategy → Explain Usage). The complete insertion sort example demonstrates the full workflow with validation through actual proof completion.	3 / 3
Progressive Disclosure	Content is well-structured with a clear overview, detailed examples inline, and appropriate references to separate files for framework-specific details (isabelle_lemmas.md, coq_lemmas.md, proof_patterns.md). References are one level deep and clearly signaled.	3 / 3
	Total	11 / 12 Passed

Description

100%

Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.

This is an excellent skill description that clearly defines a specialized niche in formal theorem proving. It provides comprehensive coverage of what the skill does (analyze proofs, propose lemmas, suggest strategies), when to use it (proof failures, stuck states, unprovable subgoals), and includes domain-specific terminology that users would naturally employ. The description is well-structured, uses third person voice correctly, and would be easily distinguishable from other skills.

Dimension	Reasoning	Score
Specificity	Lists multiple specific concrete actions: 'Analyze failed or stuck proofs', 'propose auxiliary lemmas', 'Identifies missing lemmas', 'suggests proof strategies', 'generates helper lemmas with appropriate statements and proof sketches'. Also specifies supported proof types: 'inductive proofs, case analysis, rewriting, and complex proof obligations'.	3 / 3
Completeness	Clearly answers both what ('Analyze failed or stuck proofs and propose auxiliary lemmas...Identifies missing lemmas, suggests proof strategies, and generates helper lemmas') AND when ('Use when encountering proof failures, stuck proof states, unprovable subgoals, or when needing to strengthen induction hypotheses') with explicit trigger guidance.	3 / 3
Trigger Term Quality	Includes natural keywords users would say: 'proof failures', 'stuck proof states', 'unprovable subgoals', 'strengthen induction hypotheses', 'Isabelle/HOL', 'Coq', 'auxiliary lemmas', 'helper lemmas'. These are terms a theorem prover user would naturally use when encountering these problems.	3 / 3
Distinctiveness Conflict Risk	Highly distinctive niche targeting formal theorem proving in specific proof assistants (Isabelle/HOL, Coq). The combination of 'auxiliary lemmas', 'proof failures', 'stuck proof states', and specific proof assistant names creates a clear, non-conflicting trigger profile that wouldn't overlap with general coding or documentation skills.	3 / 3
	Total	12 / 12 Passed

Validation

100%

Warnings & errors only

Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.

Validation — 11 / 11 Passed

Validation for skill structure

No warnings or errors.

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

Reviewed: 4 months ago

Table of Contents

Discovery Implementation Validation

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.