name: isabelle-hol-interface description: Interface with Isabelle/HOL for classical mathematics formalization allowed-tools:
- Bash
- Read
- Write
- Edit
- Glob
- Grep metadata: specialization: mathematics domain: science category: theorem-proving phase: 6
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
- Isar Proofs: Write structured proofs with have/show/proof
- Automation: Use Sledgehammer for ATP assistance
- Libraries: Access AFP for reusable formalizations
- Abstraction: Use locales for modular theories
Tools/Libraries
- Isabelle
- Archive of Formal Proofs (AFP)
- Sledgehammer ATPs
- Isabelle/jEdit