Agent-Skills.md

Agent Skills: Isabelle/HOL Interface

Interface with Isabelle/HOL for classical mathematics formalization

theorem-provingID: a5c-ai/babysitter/isabelle-hol-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/library/specializations/domains/science/mathematics/skills/isabelle-hol-interface

Skill Files

Browse the full folder contents for isabelle-hol-interface.

Download Skill

Loading file tree…

library/specializations/domains/science/mathematics/skills/isabelle-hol-interface/SKILL.md

Skill Metadata

Name
isabelle-hol-interface
Description
Interface with Isabelle/HOL for classical mathematics formalization

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