## 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. The main
application is the formalization of mathematical proofs and in
particular *formal verification*, which includes proving
the correctness of computer hardware or software and proving
properties of computer languages and protocols.

Compared with similar tools, Isabelle's distinguishing feature is its flexibility. Most proof assistants are built around a single formal calculus, typically higher-order logic. Isabelle has the capacity to accept a variety of formal calculi. The distributed version supports higher-order logic but also axiomatic set theory and several other formalisms. See logics for more details.

Isabelle is a joint project between Lawrence C. Paulson (University of Cambridge, UK) and Tobias Nipkow (Technical University of Munich, Germany).

## What Isabelle offers

Isabelle provides excellent notational support: new notations can be introduced, using normal mathematical symbols. Proofs can be written in a structured notation based upon traditional proof style, or more straightforwardly as sequences of commands. Definitions and proofs may include TeX source, from which Isabelle can automatically generate typeset documents.

The main limitation of all such proof systems is that proving
theorems requires much effort from an expert user. Isabelle
incorporates some tools to improve the user's productivity by
automating some parts of the proof process. In particular,
Isabelle's *classical reasoner* can perform long chains
of reasoning steps to prove formulas. The *simplifier*
can reason with and about equations. Linear *arithmetic*
facts are proved automatically.

Isabelle comes with a large theory library of formally verified mathematics, including elementary number theory (for example, Gauss's law of quadratic reciprocity), analysis (basic properties of limits, derivatives and integrals), algebra (up to Sylow's theorem) and set theory (the relative consistency of the Axiom of Choice). Also provided are numerous examples arising from research into formal verification.

With *Isar*, Isabelle offers a concise proof formulation language
which enables a user to write proof scripts naturally understandable for
both humans *and* computers.

Isabelle is closely integrated with the ProofGeneral user interface, which eases the task of writing and maintaining proof scripts.

## Preview

We provide a hyperlinked preview demonstrating Isabelle and ProofGeneral, in QuickTime format, and also as a non-hyperlinked preview in PDF.

Ample documentation is available about using Isabelle and its inner concepts, including a Tutorial published by Springer-Verlag.

## Projects

There is an (incomplete) list of past and present projects undertaken using Isabelle available.

## License

Isabelle is distributed free of charge under the open source BSD license. You may use any of our mirrors for download.