Isabelle

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: Isabelle2020 (April 2020)

Some notable changes:

• PIDE: much faster startup of Isabelle/jEdit thanks to more scalable session directory structure.
• PIDE: updated Isabelle/VSCode to follow recent moves of VSCode.
• Pure: improved treatment of theorem dependencies and proof terms, accessible via command thm_deps.
• Pure: proper treatment of oracles within internal proof objects, accessible via command thm_oracles.
• HOL: various library improvements.
• HOL: better organization of HOL-Analysis vs. HOL-Complex_Analysis.
• ML: more scalable export artifacts via XML blobs.
• Scala: support for external IDEs based on Gradle (e.g. IntelliJ IDEA).
• Scala: support for Ubuntu server applications (Linux-Apache-MySQL-PHP).
• System: Isabelle/Phabricator as self-hosted project management platform.
• System: update to current Poly/ML 5.8.1 with improved robustness, especially on Windows.
• System: improved support for macOS, notably 10.15 Catalina.

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 ample documentation, the Isabelle community Wiki, Stack Overflow, and in particular the following mailing lists:

• [email protected] 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.
• [email protected] 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).