Individual skill

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.

skills/proof-trace-summarizer/SKILL.md

Read pinned source

Source commit 4f38503747e0617504bce5329283ef837d375c09

What was checked

Matches the observed repository HEAD: Yes
Scanner rules are current: No
Repository scan complete: No
Skill scan complete: Yes
Observed behavior: Not checked yet
Last checked: Nov 6, 2026

These are observations at the recorded commit, not a guarantee of safety. Review the source before running it.

Install this skill

Choose an agent in your Stack or copy a command below. Commands fetch the pinned commit and copy only this skill directory. Existing destinations are refused. Copying a command does not install anything.

An install command is unavailable: current rules, complete repository and skill scans, an eligible behavior level and a permitted license are required.

Repository context

Repository stars (not skill ratings): 260
Repository last updated: Aug 21, 2026
License: Apache-2.0

Observed agent integration: No specific integration evidence. Standard SKILL.md installation does not imply verified compatibility.

claude-skills Repository topic
metaprogramming Repository topic
software-development Repository topic
software-engineering Repository topic
claude Repository topic
claude-code Repository topic
engineering Derived category

Files and excerpt

File metadata and permitted, redacted excerpts come from the recorded scan. Source links are pinned to that commit.

Browse files

SKILL.mdcore · 9,769 bytes
references/summarization_patterns.mddoc · 7,419 bytes
references/tactic_interpretation.mddoc · 9,289 bytes

Read excerpt


# 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