proof-trace-summarizer
Summarize long Isabelle or Coq proof scripts into high-level logical steps and reasoning flow. Use when users need to: (1) Understand the structure of a complex proof, (2) Document proof strategies for others, (3) Extract the key reasoning steps from verbose proof scripts, (4) Create readable proof outlines from detailed tactical proofs. Produces hierarchical outlines with moderate detail showing proof structure, main cases, key lemmas, and reasoning flow for both Isabelle/Isar and Coq proofs.
Profile →npx skills add majiayu000/claude-skill-registry --skill proof-trace-summarizer --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.
# Proof Trace Summarizer Summarize long proof scripts into high-level logical steps and reasoning flow. ## Overview This skill transforms verbose Isabelle or Coq proof scripts into clear, hierarchical summaries that capture the essential reasoning structure. It identifies proof patterns (induction, case analysis, equational reasoning), extracts key steps, and presents them in a readable outline format. ## How to Use Provide a proof script with: 1. **System**: Isabelle or Coq 2. **Proof script**: The complete proof to summarize 3. **Context** (optional): Theorem statement, definitions, or background The skill will produce a hierarchical outline showing: - Main proof strategy - Case structure (if applicable) - Key reasoning steps - Important lemmas or facts used ## Summarization Workflow ### Step 1: Identify Proof Structure Recognize the high-level proof pattern: **Induction proof**: Look for `proof (induction ...)` (Isabelle) or `induction ... as [|...]` (Coq) **Case analysis**: Look for `proof (cases ...)` (Isabelle) or `destruct ... as [...]` (Coq) **Direct proof**: Sequential reasoning without major branching **Equational reasoning**: Chain of rewrites or calculations **Hybrid**:
- Overview
- How to Use
- Summarization Workflow
- Step 1: Identify Proof Structure
- Step 2: Extract Major Components
- Step 3: Group Related Steps
- Step 4: Create Hierarchical Outline
- Step 5: Add Moderate Detail
- Example: Isabelle Induction Proof
- Example: Coq Case Analysis
- Example: Complex Nested Proof
- Common Proof Patterns
- Pattern: Proof by Simplification
- Pattern: Proof by Induction
What does the proof-trace-summarizer skill do?
Summarize long Isabelle or Coq proof scripts into high-level logical steps and reasoning flow. Use when users need to: (1) Understand the structure of a complex proof, (2) Document proof strategies for others, (3) Extract the key reasoning steps from verbose proof scripts, (4) Create readable proof outlines from detailed tactical proofs. Produces hierarchical outlines with moderate detail showing proof structure, main cases, key lemmas, and reasoning flow for both Isabelle/Isar and Coq proofs.
How do I install it?
Run `npx skills add majiayu000/claude-skill-registry --skill proof-trace-summarizer --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.