library-advisor

Recommend 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.

1.03x

Quality

92%

Does it follow best practices?

Impact

96%

1.03x

Average score across 3 eval scenarios

Securityby

Passed

No findings from the security scan

Preview

This is a new way to view eval results. We're still working on it, so the layout may change.

Run	Type	Date	Status
baseline vs usage-spec With / without context 7 months ago Completed	With / without context	7 months ago	Completed

Eval run

019cc498-204c-71a8-bbb6-3a8b5513f65e

Run 7 months ago

Stats are not available yet

The run is available. Its result stats will appear here when they are ready.

Repository: ArabelaTso/Skills-4-SE
Path: skills/library-for-proof-advisor/SKILL.md
Commit: 4f38503

Evaluated: 7 months ago
Agent: Claude Code
Model: Claude Sonnet 4.6

Table of Contents

Coq Proof Assistance: List Properties Isabelle/HOL Arithmetic Proofs: Lemma Discovery and Proof Strategies Library Advisor: Combined List and Set Proofs

Is this your skill?

If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.