Agent-Skills.md

Agent Skills: Theorem Prover Interface

Interface with interactive theorem provers for mechanized verification

formal-verificationID: a5c-ai/babysitter/theorem-prover-interface

Repository

a5c-ai/babysitter
a5c-aiLicense: MIT
244

Install this agent skill to your local

pnpm dlx add-skill https://github.com/a5c-ai/babysitter/tree/HEAD/plugins/babysitter/skills/babysit/process/specializations/domains/science/computer-science/skills/theorem-prover-interface

Skill Files

Browse the full folder contents for theorem-prover-interface.

Download Skill

Loading file tree…

plugins/babysitter/skills/babysit/process/specializations/domains/science/computer-science/skills/theorem-prover-interface/SKILL.md

Skill Metadata

Name
theorem-prover-interface
Description
Interface with interactive theorem provers for mechanized verification

Theorem Prover Interface

Purpose

Provides expert guidance on using interactive theorem provers for mechanized formal verification.

Capabilities

  • Coq proof script generation
  • Isabelle/HOL interface
  • Lean 4 integration
  • Proof automation (hammers, tactics)
  • Proof library search
  • Extraction to executable code

Usage Guidelines

  1. Prover Selection: Choose appropriate theorem prover
  2. Formalization: Formalize definitions and theorems
  3. Proof Development: Develop proofs interactively
  4. Automation: Apply automated tactics
  5. Extraction: Extract certified code if needed

Tools/Libraries

  • Coq
  • Isabelle
  • Lean
  • ACL2