What is Isabelle?
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle was originally developed at the University of Cambridge and Technische Universität München, but now includes numerous contributions from institutions and individuals worldwide. See the Isabelle overview for a brief introduction.
Now available: (December 2021)
- - Download for Linux + Download for Linux (Intel) + +
- + + + + Download for Linux (ARM)
- Download for Windows
- Download for macOS
Hardware requirements:
- Small experiments: 4 GB memory, 2 CPU cores
- Medium applications: 8 GB memory, 4 CPU cores
- Large projects: 16 GB memory, 8 CPU cores
- Extra-large projects: 64 GB memory, 16 CPU cores
Some notable changes:
- HTML presentation now includes links to formal entities.
- Isar: local theory support for syntax and no_syntax commands.
- Isabelle/jEdit: distribution of original jEdit editor with Isabelle/Scala modules and plugins.
- HOL: new order prover.
- HOL: many changes and improvements on bit operations and word types.
- HOL: various library improvements (HOL-Library, HOL-Combinatorics, HOL-Analysis, HOL-Statespace)
- Sledgehammer: update of ATPs and SMTs: E prover, veriT, Zipperposition, Vampire (now with Open-Source license).
- Nitpick: external MiniSat solver for all supported Isabelle platforms.
- ML: uniform treatment of external processes via Isabelle/Scala.
- ML: advanced antiquotations for Type/Const constructors, and for inline instantiation of types, terms, facts.
- Haskell: substantially improved Isabelle/Haskell library.
- System: more predefined Isabelle symbols (blackboard-bold, Z notation).
- System: support for Isabelle/Scala modules defined in user-space.
- System: improved document preparation using Isabelle/Scala.
- System: update to current OpenJDK 17 (LTS) and Poly/ML 5.9 (with preliminary support for arm64).
See also the cumulative NEWS.
Distribution & Support
Isabelle is distributed for free under a conglomerate of open-source licenses, but the main code-base is subject to BSD-style regulations. The application bundles include source and binary packages and documentation, see the detailed installation instructions. A vast collection of Isabelle examples and applications is available from the Archive of Formal Proofs.
Support is available by the official documentation and mailing lists:
- isabelle-users@cl.cam.ac.uk provides a forum for Isabelle users to discuss problems, exchange information, and make announcements. Users of official Isabelle releases should subscribe or see the archive.
- isabelle-dev@in.tum.de covers the Isabelle development process, including intermediate repository versions, and administrative issues concerning the website or testing infrastructure. Early adopters of development snapshots or repository versions should subscribe or see the archive.
Zulip Chat is a real-time discussion platform to exchange ideas, ask questions, and collaborate on Isabelle projects, with minimalistic public archive.
Stack Overflow is a question-and-answer platform, with complex review process but limited discussion facilities.