tactic-suggestion-assistant
From the author
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.
Install
npx skills add ArabelaTso/Skills-4-SE --skill tactic-suggestion-assistant -a claude-code
Installs to .claude/skills/tactic-suggestion-assistant/ · Each command fetches the skill straight from GitHub with the open skills CLI.
Byte-identical to the scanned commit, with the repository’s licence and a SOURCE.txt.
Want your agent to suggest skills while you type? See how to use skills from your IDE.
Safety checks on SKILL.md
No warnings.
Why 83
aiqbench computes the trust score from public signals. It is not a security audit, so read a skill before you install it.
Similar skills
Closest to this one by what they do and when they are used.
- lemma-discovery-assistantArabelaTso/Skills-4-SEAnalyze 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.Other★ 258
- library-advisorArabelaTso/Skills-4-SERecommend relevant Isabelle/HOL or Coq standard library theories, lemmas, and tactics based on proof goals. Use when: (1) Users need library lemmas for their proof, (2) Proof goals match standard library patterns, (3) Users ask what libraries to import, (4) Specific lemmas are needed for list/set/arithmetic operations, (5) Users are stuck and need to know what library support exists, or (6) Guidance on find_theorems/Search commands is needed. Supports both Isabelle/HOL and Coq standard libraries.Planning★ 258
- proof-failure-explainerArabelaTso/Skills-4-SEAnalyze and explain why Isabelle or Coq proofs fail, identifying the root cause such as type mismatches, missing assumptions, incorrect goals, unification failures, or inapplicable tactics. Use when the user encounters proof failures, error messages in formal verification, stuck proof states, or asks why their Isabelle/Coq proof doesn't work.Other★ 258
- proof-trace-summarizerArabelaTso/Skills-4-SESummarize 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.Productivity★ 258
- proof-refactoring-assistantArabelaTso/Skills-4-SERestructure and improve Isabelle or Coq proofs to enhance readability, modularity, and maintainability without changing semantics. Use when proofs are long and monolithic, have repeated patterns, use unclear naming, lack documentation, or when the user asks to refactor, clean up, improve, or reorganize their formal proofs.Engineering★ 258
- proof-skeleton-generatorArabelaTso/Skills-4-SEGenerate structured proof skeletons with tactics, strategies, and intermediate lemmas for theorems in Isabelle/HOL or Coq. Use when users need to: (1) Create proof outlines for theorem statements, (2) Generate proof structure with tactic placeholders, (3) Identify key lemmas needed for a proof, (4) Plan proof strategies (induction, case analysis, forward/backward reasoning), (5) Scaffold proofs with intermediate steps and subgoals, or (6) Convert theorem statements into detailed proof templates. Supports both Isabelle/HOL and Coq equally.Planning★ 258
Ratings & reviews
—
no reviews
Tried this skill? Rate it to help others. Sign in
Discussion
Join the discussion. Sign in