The HOL Light theorem prover

There are a number of versions of HOL, going back to Mike Gordon's work in the early 80s. Compared with other HOL systems, HOL Light uses a much simpler logical core and has little legacy code, giving the system a simple and uncluttered feel. Despite its simplicity, it offers theorem proving power comparable to, and in some areas greater than, other versions of HOL, and has been used for some significant industrial-scale verification applications.

You can download the sources for the latest version 2.20 here. It should work on pretty much any platform under most recent versions of Ocaml. (Note that it doesn't yet work under the very latest OCaml, 3.10, owing to changes to camlp4. HOL Light will be updated soon, but meanwhile use a version ≤ 3.09.3.) See the README file in the distribution for detailed installation instructions.

Experimental Linux binaries for version 2.20 are now available, created using CryoPID. NB: I'm not sure how portable these are across Linux versions; better to build from source if you can. The files are hol (core system), hol.sosa (preloaded with analysis and sum-of-squares tools), hol.multivariate (preloaded with multivariate analysis) and hol.card (preloaded with cardinal arithmetic). Note that although these work as standalone executables, if you are planning to work much with the system, you'll probably still want to download the HOL sources to give access to additional library directories and to the help files. For example, if you download the HOL Light source tree to "/home/myself/hol_light", you might start a HOL Light session with the following so that HOL Light can find all the files (# is the OCaml prompt):

   # hol_dir := "/home/myself/hol_light";;
   val it : unit = ()
   # load_path := ["."; !hol_dir];;
   val it : unit = ()

• Reference Manual available as online crosslinked HTML or as one PDF file.
• Tutorial, which tries to teach HOL Light through examples.
• Quick Reference Guide compiled by Freek Wiedijk (text, PDF, Postscript, DVI, LaTeX)
• Summary of many HOL source files, written by Carl Witty (text)
• Old user manual, not fully updated from the older CAML Light version (DVI, Postscript and PDF).
• The hol-info mailing list is a good place for HOL-related discussion
• Josef Urban's HOL Proof Advisor uses automated data mining to produce proof advice.

• Formalization of floating-point arithmetic, and the formal verification of several floating-point algorithms at Intel.
  See this paper for a quick summary and more references, and this one for a more detailed presentation.
• The Flyspeck project to machine-check Tom Hales's proof of the Kepler conjecture.
  Tom has already proved the Jordan Curve Theorem and other relevant results in HOL Light.
• Many other mathematical results of varying degrees of difficulty have been verified in HOL Light.
  See for example the HOL Light entries on the Formalizing 100 Theorems page.