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: Isabelle2024 (May 2024)

Hardware requirements:

Some notable changes:

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:

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.