ekirton

Compress Proof — Development skill for Claude Code

Development community

Given a working Coq proof, systematically search for shorter or cleaner alternatives using hammer tactics, lemma search, and tactic chain simplification.

How to install Compress Proof

Installs to ~/.claude/skills/ekirton-poule-compress-proof/SKILL.md

Terminal

mkdir -p ~/.claude/skills/ekirton-poule-compress-proof && curl -fsSL https://raw.githubusercontent.com/ekirton/Poule/HEAD/commands/compress-proof.md -o ~/.claude/skills/ekirton-poule-compress-proof/SKILL.md

Restart Claude Code, or start a new session, for it to be picked up.

What Compress Proof does

Given a working Coq proof, systematically search for shorter or cleaner alternatives using hammer tactics, lemma search, and tactic chain simplification. Present verified alternatives ranked against the original. Never modify the original file unless the user explicitly chooses a replacement.

Identify the target proof

The user will specify a proof by name (e.g., `my_lemma`), by file location (e.g., `src/Foo.v:42`), or by asking you to compress the proof at point in the current context. If t

Alternatives in Development

Rank — /rank - Triage Scraped Jobs into a Ranked Shortlist 36.6k ★
Breach Check — HIBP k-anonymity check on a password wordlist 4.5k ★
Fidelity — Measure how faithfully a clone reproduces a site — pixel-diff plus motion-fidelity into one 0-100 score, a let 3.6k ★