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: Isabelle2018 (August 2018)
Some notable changes:
- Improved infix notation within terms.
- Improved syntax for formal comments, within terms and other languages.
- Improved management of ROOT files and session-qualified theories.
- Various improvements of document preparation.
- Many Isabelle/jEdit improvements, including semantic IDE for BibTeX.
- Numerous HOL library improvements, including HOL-Algebra.
- Substantial additions to HOL-Analysis.
- HOL-Library.Code_Lazy: code generation for lazy evaluation.
- HOL-Real_Asymp: tools for semi-automatic real asymptotics.
- Isabelle server for reactive communication with other programs.
- More uniform 64-bit platform support: smaller Isabelle application.
See also the cumulative NEWS.
Warning: potential problem with Ubuntu Linux 18.04
The kernel update linux-image-4.15.0-36-generic
(Oct-2018) introduces a timing problem with socket communication in the Isabelle Prover IDE, notably Isabelle/jEdit. Thus loading big sessions becomes very slow (e.g. theory HOL-Library.Library
or HOL-Analysis.Analysis
). This can be avoided by downgrading to linux-image-4.15.0-34-generic
or by using the following temporary workaround for Isabelle2018.
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 ample documentation, the Isabelle community Wiki, Stack Overflow, and in particular the following mailing lists:
- {isabelle-users} AT [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} AT [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 (also available at mail-archive.com).