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.
npx skills add majiayu000/claude-skill-registry --skill lemma-discovery-assistant --agent claude-code
Same command for any agent — swap --agent for codex, cursor, copilot.
Weekly change comes from our own snapshots, not the repository page — it measures attention, not adoption.
# Lemma Discovery Assistant Analyze stuck or failed proofs and propose auxiliary lemmas that can help complete the proof. ## Overview When proofs fail or get stuck, the issue is often a missing auxiliary lemma. This skill helps identify what lemmas are needed by: 1. Analyzing the current proof state and goal 2. Identifying gaps in reasoning 3. Proposing auxiliary lemmas with precise statements 4. Suggesting proof strategies for the lemmas 5. Explaining how the lemmas help the main proof ## When Proofs Get Stuck ### Common Symptoms **Unprovable subgoal:** - Tactics fail to make progress - Goal seems "obviously true" but won't prove - Missing connection between hypotheses and goal **Weak induction hypothesis:** - Induction step fails - Need stronger property to prove - Generalization required **Missing intermediate steps:** - Large gap between current state and goal - Need stepping stones - Complex reasoning required **Insufficient rewrite rules:** - Simplification doesn't go far enough - Need additional equations - Definitions need unfolding lemmas ## Lemma Discovery Process ### Step 1: Analyze Proof State Examine the current proof context: **What to look for:** - Current goal state
- Overview
- When Proofs Get Stuck
- Common Symptoms
- Lemma Discovery Process
- Step 1: Analyze Proof State
- Step 2: Identify the Gap
- Step 3: Propose Lemma Statement
- Step 4: Suggest Proof Strategy
- Step 5: Explain Usage
- Lemma Patterns by Proof Type
- Inductive Proofs
- Generalization Lemmas
- Rewrite Lemmas
- Structural Lemmas
What does the lemma-discovery-assistant skill do?
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.
How do I install it?
Run `npx skills add majiayu000/claude-skill-registry --skill lemma-discovery-assistant --agent claude-code` — it drops the skill into your project so the agent can pick it up. Swap the --agent value for codex, cursor or copilot if you use one of those.
Where does this skill come from?
From majiayu000/claude-skill-registry, a repository with 534 stars. We read it straight from the repository tree rather than a submitted listing, so what you see here is what is actually published.
Is a popular skill a good skill?
Not necessarily. Stars measure attention, not adoption — a repository can trend for a week and be abandoned. That is why we show the weekly change from our own snapshots next to the total, instead of a single flattering number.