Isabelle Hol Interface

Interface with Isabelle/HOL for classical mathematics formalization

a5c-ai Updated 1.7k repo stars

File contents

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

a5c-ai/babysitter/tree/main/library/specializations/domains/science/mathematics/skills/isabelle-hol-interface commit 9d35560853

Frequently asked questions

npx skillmds@latest add a5c-ai/isabelle-hol-interface