Isabelle is a proof assistant. Its main application is HOL. Related proof assistants are HOL4, HOL Light, HOL Zero, and ProofPower. These are programmed, as Isabelle itself, in ML. In contrast to other proof assistants, Isabelle is based on classical set theoretic foundations. The Archive of Formal Proofs is an online library of proofs formalized in Isabelle.

proof assistants:

based on plain type theory/set theory:

based on dependent type theory/homotopy type theory:

For monoidal category theory:

For higher category theory:

projects for formalization of mathematics with proof assistants:

Historical projects that died out:


Implementation of homotopy type theory in Isabelle:

category: software