OpenSkillIndex← back to search
claude-codescience

Babysitter isabelle-hol-interface

Interface with Isabelle/HOL for classical mathematics formalization

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/mathematics/skills/isabelle-hol-interface" ~/.claude/skills/a5c-ai-babysitter-isabelle-hol-interface && rm -rf "$T"
manifest: library/specializations/domains/science/mathematics/skills/isabelle-hol-interface/SKILL.md
tags
#theorem-proving#mathematics#formalization#isabelle#proof-assistant#logic
source content

Isabelle/HOL Interface

Purpose

Provides expert guidance on using Isabelle/HOL for classical mathematics formalization and theorem proving.

Capabilities

  • Isar structured proof generation
  • Sledgehammer automated theorem proving
  • Archive of Formal Proofs access
  • Locales and type classes
  • Code generation to SML/Haskell

Usage Guidelines

  1. Isar Proofs: Write structured proofs with have/show/proof
  2. Automation: Use Sledgehammer for ATP assistance
  3. Libraries: Access AFP for reusable formalizations
  4. Abstraction: Use locales for modular theories

Tools/Libraries

  • Isabelle
  • Archive of Formal Proofs (AFP)
  • Sledgehammer ATPs
  • Isabelle/jEdit