### Interactive Theorem Proving

The HOL System Tutorial is a fairly gentle introduction to using the system HOL. It provides screenshots from the interactive sessions, so you can follow what’s happening even if you don’t have the system installed. Better still, download and install HOL, then follow the tutorial to verify the sessions and get a hands-on experience with the system.

The first substantial example is a proof of this theorem: that there are infinitely many primes. The classic proof by Euclid is considered as a proof from “The Book” — in which God keeps the most elegant proof of each mathematical theorem, according to the mathematician Paul Erdös. During a lecture in 1985, Erdös said, “You don’t have to believe in God, but you should believe in The Book.”

However, to rephrase this proof in HOL, many basic concepts needs to be established first: what is a prime? how to define divisibility? All these boil down to logical statements about natural numbers.

The actual proof process in HOL is assisted by the Proof Manager. There are actions to put a goal to the manager, expand the goal by tactics, which are strategies to pick either known facts or lemma from a HOL theory. The expansion of a goal usually gives subgoals, which can be further expanded until everything is known, upon which the initial goal is proved. Of course, picking the correct strategies take some understanding and experience. The Proof Manager allows you to advance a step, backup a step, or redo from the start. All these techniques are demonstrated in this example of the Tutorial.

In the end, Euclid’s proof of the infinity of primes is done in about 10 lines of HOL code, after much polishing. This is finale of a whole chapter with more than 30 pages!