# Isabelle Hol Interface

> Interface with Isabelle/HOL for classical mathematics formalization

- Skill: `a5c-ai/isabelle-hol-interface` (Agent Skill)
- Install (CLI): `npx skillmds@latest add a5c-ai/isabelle-hol-interface`
- Raw SKILL.md: https://api.skillmd.com/api/skills/a5c-ai/isabelle-hol-interface/raw
- Safety review: pending (external: skill-scanner PASS, skillspector PASS)
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- Author: a5c-ai (https://skillmd.com/u/a5c-ai)
- Updated: 2026-09-09
- Page: https://skillmd.com/skills/a5c-ai/isabelle-hol-interface

---


# 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