Individual skill

tactic-suggestion-assistant

Analyze proof states in Isabelle or Coq and suggest applicable tactics to make progress. Use when users need help with: (1) Choosing the next tactic in an interactive proof, (2) Understanding what tactics apply to their current goal, (3) Getting unstuck in a proof, (4) Learning which tactics work for specific goal structures (conjunctions, implications, induction, etc.). Provides 3-5 ranked tactic suggestions with explanations for intermediate-level proofs in both Isabelle/Isar and Coq.

skills/tactic-suggestion-assistant/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
education 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 · 8,002 bytes
references/coq_tactics.mddoc · 7,874 bytes
references/isabelle_tactics.mddoc · 6,231 bytes
references/proof_patterns.mddoc · 10,356 bytes

Read excerpt


# Tactic Suggestion Assistant

Analyze proof states and suggest applicable tactics to make progress in Isabelle or Coq.

## Overview

This skill helps you navigate interactive proofs by analyzing the current proof state and suggesting 3-5 ranked tactics that can make progress. It works with both Isabelle/Isar and Coq, providing system-specific suggestions with explanations.

## How to Use

Provide the current proof state including:
1. **System**: Isabelle or Coq
2. **Goal**: The current goal to prove
3. **Context**: Available hypotheses/assumptions (if any)