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: Isabelle2025-1 (December 2025)
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:
- PIDE: load markup from background session image (e.g. theory
HOL.Nat). - Isabelle/jEdit: support for command-line system options (
-o). - Isabelle/jEdit: support for dark mode and screen readers.
- Isabelle/jEdit: built-in navigator, without requiring plugins.
- Isabelle/jEdit: more reactive mouse handling, notably on macOS.
- Isabelle/jEdit: updated FlatLaf GUI L&F with scalable SVG icons.
- Isabelle/jEdit: improved appearance on Linux (GUI scaling) and macOS (L&F).
- Isabelle/VSCode: more robust session build process on console.
- Isabelle/VSCode: GUI panels for Documentation, Symbols, Sledgehammer.
- Isabelle/VSCode: update of underlying VSCodium distribution.
- HOL: various improvements of theory libraries.
- HOL: various improvements to code generation.
- HOL: updates and improvements of Sledgehammer and external provers.
- HOL: generation of running time functions for HOL functions.
- System: ML settings may depend on command-line system options (
-o). - System: command-line tool to process theories within adhoc session.
- System: more detailed build progress.
- System: more robust build cluster management.
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 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.
- 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 (with alternative repository clone) 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.


Download for Linux (Intel)
Download for Windows
Download for macOS