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-assistant94
Does it follow best practices?
Validation for skill structure
Discovery
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 |
Implementation
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 |
Validation
100%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.
- Reviewed
Table of Contents
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.