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: (October 2022)
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 is more robust and covers more files and links.
- Display of instantiation for schematic goals.
- PIDE: improved Isabelle/VSCode based on bundled VSCodium engine.
- HOL: various improvements of theory libraries.
- HOL: updates and improvements of Sledgehammer.
- HOL: improved simproc support for record types.
- ML: scalable type Bytes.T with support for XZ compression.
- System: bundled Node.js/Chromium/Electron platform (via VSCodium).
- System: Isabelle/Scala is based on Scala 3 (dotty compiler).
- System: tools to sync hg repositories, notably Isabelle + AFP.
- System: improved "isabelle log" tool with regex filtering.
- System: more robust SSH support in Isabelle/Scala.
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:
-
-
- The The isabelle-users mailing list 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 +
- The isabelle-dev + mailing list 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 and Stack Exchange are a question-and-answer platform, with complex review process but limited discussion facilities.