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: (February 2021)
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:
- Improved HTML presentation in Isabelle/Scala, using PIDE markup.
- Improved PDF document preparation in Isabelle/Scala, using LuaLaTeX.
- Isabelle/jEdit: improved monitoring of Java and ML process.
- Isabelle/jEdit: improved look-and-feel and IDE feedback.
- Pure: improved handling of named contexts and local syntax bundles.
- HOL: substantially reworked support for Word library.
- HOL: various syntax and library improvements.
- HOL: various Sledgehammer and SMT improvements, with updated external tools.
- HOL: support for Nitpick/Kodkod in Isabelle/Scala.
- ML: routine support for Isabelle/Scala functions in Isabelle/ML.
- System: support for Isabelle/Scala services defined in user-space.
- Support for macOS Big Sur on Intel and Apple Silicon (ARM).
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 - (also available - at mail-archive.com). + 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.