The HOL Light theorem prover
Written by John Harrison drawing
on the work of
Mike Gordon Tom Melham Robin Milner Larry Paulson Konrad Slind
and many other HOL
and LCF researchers
HOL Light is a computer program to help users prove interesting mathematical
theorems completely formally in higher order logic. It sets a very exacting
standard of correctness, but provides a number of automated tools and
pre-proved mathematical theorems (e.g. about arithmetic, basic set theory and
real analysis) to save the user work. It is also fully programmable, so users
can extend it with new theorems and inference rules without compromising
its soundness. 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.
HOL Light is now hosted on
Github so you can get the sources from the Github repository. You can
browse individual source files online, or check out all the code using git. For
example, the following command will copy all the code from the
Github repository into a new directory hol-light (assumed not to exist
git clone https://github.com/jrh13/hol-light.git
If you use a debian-based Linux distribution, then you can get a ready-to-use
HOL Light system together with useful auxiliary tools simply by installing the
hol-light package (thanks to Hendrik Tews
). For example
sudo apt-get install hol-light
Otherwise, you can always install it yourself. HOL Light is written in Objective CAML (OCaml), and
it should work with any reasonably recent version. To build with OCaml 3.10 and
later you will also need to install camlp5, version 5.07 or
higher. See the README file in the distribution for detailed installation
The following lists some available documentation and resources:
Here are some applications of HOL Light:
- Reference Manual available as online crosslinked
HTML or as one PDF file (also an older variant keyed to version 2.20).
- Tutorial, which
tries to teach HOL Light through examples.
- Quick Reference Guide compiled by
- Jeremy Bem's hol-online,
and the earlier project Formalpedia, use a
processed version of HOL Light to produce an online repository of software and
- Summary of many HOL source files,
written by Carl Witty (text)
- Old user manual, not fully updated from the older CAML Light
- 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.
HOL Light is free open source software. It comes with no warranty of any kind
(see the LICENCE file in the distribution), and no guarantee of maintainance.
However, please feel free to send any comments or questions to the author at
- 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
- 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.
Last updated by John Harrison
on Fri 13th January 2017.