OpenSkillIndex← back to search
claude-codescience

Babysitter theorem-prover-interface

Interface with interactive theorem provers for mechanized verification

install
source · Clone the upstream repo
git clone https://github.com/a5c-ai/babysitter
Claude Code · Install into ~/.claude/skills/
T=$(mktemp -d) && git clone --depth=1 https://github.com/a5c-ai/babysitter "$T" && mkdir -p ~/.claude/skills && cp -r "$T/library/specializations/domains/science/computer-science/skills/theorem-prover-interface" ~/.claude/skills/a5c-ai-babysitter-theorem-prover-interface && rm -rf "$T"
manifest: library/specializations/domains/science/computer-science/skills/theorem-prover-interface/SKILL.md
tags
#theorem-proving#formal-verification#coq#isabelle#lean#proof-automation
source content

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