The simplest way to run HilbertAxiom.ml is this.
In a terminal window (or Emacs shell), move to your hol_light directory and paste in
these 3 commands, followed by a RETURN:
ocaml
#use "hol.ml";;
#use "RichterHilbertAxiomGeometry/make.ml";;

This will not work if you have already evaluated HilbertAxiom_read.ml,
because you will get an error
Exception: Failure "new_type: type point has already been declared".

You will see 190 or so definitions and proved theorems, in perhaps 15
minutes.  

How to check the Hilbert axiomatic geometry proofs HilbertAxiom.ml,
which are a formalization in the proof assistant HOL Light of
http://www.math.northwestern.edu/~richter/hilbert.pdf using Freek
Wiedijk's Mizar mode miz3.  This has only been checked on Linux.  I'll
also assume familiarity with the Emacs editor (version 23 or 24).

First a discussion of miz3.  There are a number of good proof
assistants to formalize mathematical proofs in, e.g. Coq, with which
the 4-color theorem proof was formalized.  There are a number of good
HOL proof assistants, e.g. HOL4 & Isabelle.  Two outstanding
advantages of HOL Light are Freek's miz3 and that HOL Light is the
preferred proof assistant of Tom Hales, who is ambituously trying to
formalize his proof of the Kepler sphere-packing theorem.  I suspect
that John Harrison's leadership is involved in both advantages.  

Mizar was the first proof assistant allowing readable formal
proofs. Miz3 now allows readable formal proofs in HOL Light.  Miz3
mostly resembles Mizar in its syntax (let, assume, thus, proof, by,
end, consider, suppose, cases, ...)  and proof structure.  The Mizar
type system and vocabulary (both quite confusing to beginners) is gone
from miz3.  As in Mizar, each line in a miz3 proof is of the form
statement by list;
so the statement is supposed to be justified by the list of results.
But the "by justification" in Mizar is quite different from that in
miz3.  The miz3 by justification is mostly performed by the HOL Light
FOL prover MESON, which is quite powerful, so in miz3, one can skip
steps that could not be skipped in Mizar, which seems to have
intentionally weakened the by justification in order to encourage
readable proofs.  Miz3 has no such intentional weakness (although
timeout must be set to a high value to skip steps), but MESON is not
particularly good at equational reasoning, as one sees in this example
from the Hilbert code (using fancy fonts for readability):

let B4 = new_axiom
  `∀ l A B C. Line l ∧ ¬Collinear A B C ∧ 
   A ∉ l ∧ B ∉ l ∧ C ∉ l ∧ 
   (∃ X. X ∈ l ∧ Between A X C) ⇒ 
   (∃ Y. Y ∈ l ∧ Between A Y B) ∨ (∃ Y. Y ∈ l ∧ Between B Y C)`;;

let B4' = thm `;
  ∀ l A B C. Line l ∧ ¬Collinear A B C ∧ 
   A ∉ l ∧ B ∉ l ∧ C ∉ l ∧ 
   (∃ X. X ∈ l ∧  X ∈ open (A,C)) ⇒
   (∃ Y. Y ∈ l ∧  Y ∈ open (A,B)) ∨ (∃ Y. Y ∈ l ∧  Y ∈ open (B,C)) 
   by IN_Interval, B4;
`;;

B4' does nothing but substitute into B4 the definition 
IN_Interval     |- ∀ A B X. X ∈ open (A,B) ⇔ Between A X B
This is equational reasoning, and B4' times out with the default
timeout value of 1 (5 suffices), and then, a longer proof is needed:

let B4prime = thm `;
  let l be point_set;
  let A B C be point;
  assume Line l ∧ ¬Collinear A B C ∧ 
  A ∉ l ∧ B ∉ l ∧ C ∉ l ∧ 
  (∃ X. X ∈ l ∧  X ∈ open (A,C))     [H1];
  thus (∃ Y. Y ∈ l ∧  Y ∈ open (A,B)) ∨ (∃ Y. Y ∈ l ∧  Y ∈ open (B,C))

  proof
    Line l ∧ ¬Collinear A B C ∧ 
    A ∉ l ∧ B ∉ l ∧ C ∉ l ∧ 
    (∃ X. X ∈ l ∧  Between A X C)     by H1, IN_Interval;
    (∃ Y. Y ∈ l ∧ Between A Y B) ∨ (∃ Y. Y ∈ l ∧ Between B Y C)     by -, B4;
  qed     by -, IN_Interval;
`;;

The biggest difference between miz3 and Mizar is that miz3 allows one
to mix the procedural and declarative styles of formal proofs (Mizar
proofs are entirely declarative).  That is, one can use HOL Light
tactics in the by list, although this is essentially not done here.  A
HOL Light tactic that might be helpful here is REWRITE_TAC, which is
used in equational reasoning, an interesting area of HOL.

It pay to write a `skeleton' of your proof before filling in the
details, and I always start with this: 

  proof

  qed     by -;

My miz3 proof typically end with "qed by ... ;", Freek's macro for
"thus thesis by ... ; end;", as in the proof of B4prime above, and
rarely with neither qed nor end, as in the short proof of B4', but a
proof with cases must end with "end".  Suppose in the course of a
proof you realize you need cases.  Write in the various cases (with
suppose) first before giving the proofs, or miz3 will give you a
skeleton error.  So your proof will then look something like this:

  proof
    [...]
    A ∨ B ∨ C;
    cases by -;
    suppose A;

    qed by -;
    suppose B;

    qed by -;
    suppose C;

    qed by -;
  end;

The point is that the final "qed by -;" matching "proof" has been
changed to "end;" Here's a partial explanation.  In miz3, there is
always a thesis, which changes from line to line.  "Thus thesis" means
the thesis is proven, and then one writes "end" to end the proof.  In
the cases construction above, each of the 3 forks have their own
thesis, A, B and C resp., and each proofs end with qed.  So in the
final line, there is no thesis!  So we merely write "end".  

In the proof B4prime above, "thus" seems to have two separate
meanings.  The first thus seems to be stating the theorem, and the
second thus (contained in the qed) is is ending the proof.  In a sense
thus has the same meaning.  Let's simplify B4prime as 
let B4prime = thm `;
  [...] 
  thus α ∨ β
  proof
  [...] 
  thus thesis by -, IN_Interval;
  end;
`;;
The entire "proof [...] IN_Interval;" is as a justification of the
statement α ∨ β, even though there is no "by".  So we could in a sense
rewrite B4prime as
let B4prime = thm `;
  [...] 
  thus α ∨ β by [...];
  end;
`;;

As the thesis is α ∨ β on the "thus" line, this is analogous to 
thus thesis by -, IN_Interval;
which ends the proof.  

My code uses a fair amount of set theory, which is explained in John's
tutorial briefly in sec 14, and in more detail in his reference
manual.  I found browsing the file sets.ml to be quite helpful.
SET_RULE, explained on p 92 of the tutorial simplified my coding.


At the top I explained how to run HilbertAxiom.ml.  For a longer
journey, comment the top t two lines of HilbertAxiom.ml and
FontHilbertAxiom.ml

verbose := false;;
report_timing := false;;

Change into the directory containing your HOL source files (named hol_light), as
explained in the HOL Light documentation.  I'll assume that you can
copy and paste with the mouse.  Open a terminal window.  Paste in
these 4 commands and type RET:

ocaml
#use "hol.ml";; 
#load "unix.cma";;
loadt "miz3/miz3.ml";;

After a short while you will see 
val it : unit = ()
#
Now select the entire file HilbertAxiom.ml and paste it in.  This will
take perhaps 15 minutes and you'll see various numbers and so forth to
indicate how hard miz3 is working.   Paste the file in again, and in
perhaps 15 seconds you will see the miz3 output, with no numbers.  The
faster speed is due to the fact that miz3 caches information.

The miz3 cache causes trouble if you change the statement of a
theorem. To clear all the theorems from the miz3 cache paste in

reset_miz3 0;;

Theorems are created by thm, and definitions are created by
new_definition.  This command will not clear definitions or axioms, so
to change a definition or axioms, end the session and start a new
session.  Sometimes even when only changing theorems it's good to
start a new session.

To end your ocam/HOL-Light/miz3 session, type
C-d 
If you paste in bad input, sometimes you can fix the problem by typing 
C-c (or the signal BREAK in an Emacs shell C-c C-c).

To learn the thesis in a statement in a miz3 proof, insert
exec GOAL_TAC; 
after the statement, and the type 
p();;
at the end of the proof. 

There are two problems with pasting into a terminal window, both
solved by using intead an Emacs shell, created with M-x shell.  After
pasting into the shell, type RET.  In a terminal window, miz3 output
is mixed with miz3 code pasted in.  More seriously, a terminal window
can only be scrolled back so far, so with a long program, errors at
the top of the file won't be visible.  When pasting into an Emacs
shell, the output is all at the end, and there is no line limit.
Freek has a different system of using miz3 involving code being piped
directly from the editor vi, but I have not tried it yet.  You should
use a separate Emacs process for each shell you use, because in the 30
seconds or so when the shell is interpreting the program, no editing
can take place in that Emacs process.

Loading the file hol-light-fonts.el (or for a bit more speed,
hol-light-fonts.elc) will put any file with extension `ml' in
text-mode with auto-fill-mode turned off (provided it isn't set to be
on by default in your .emacs file) and visual-line-mode turned on,
which turns on `word-wrap', which aids readability with my long lines.

The miz3 error messages are rather cryptic, but this seems to be a
problem with HOL Light.  Some tips on the error messages:

#1 inference error
means that miz3 asserts that your `by' justification is impossible.  A
simple way to earn a #1 error is to mix up `qed' and `end' in a cases
construction.  

#2 inference time-out
means that miz3 was unable to calculate your `by' justification before
timing out.  There are two possibilities: 
1) your `by' justification doesn't work, so you should fix it;
2) you need more time, in which case you can increase the value of
timeout, to e.g. 50 as is done here, with
timeout := 50;;
You never get a #2 time-out error if you set timeout to infinity, by
timeout := -1;;
As Freek explains, this is useful in checking ones proofs on a slower
machine than the one on which the miz3 proofs were debugged on.

#3 skeleton error
require a good understanding of miz3's version of Mizar's (barely documented) notion of the skeleton, which is the outline of the proof.  Freek's paper contains a reasonably good explanation of miz3 skeletons.  

The first line with an error message may not be the first line with a
mistake on it.  Consider this fragment of a miz3 error messages:

                                                          Exception:
Mizar_error
 (`;
    let A B C be point;
    assume ~Collinear A B C [H1];
    assume seg B A === seg C B [H2];
  ::                               #3
  :: 3: skeleton error
    thus  angle BCA  === angle CAB  
  ::                             #8
  :: 8: syntax or type error hol
  
    proof
  [...] 

There is nothing wrong with the line with the #3 error message.  The
problem is in the next line with the #8 error, where `BCA' & `CAB'
should read `B C A' and `C A B'.  One this problem is fixed, the earlier #3 error disappears:

Mizar_error
 (`;
    let A B C be point;
    assume ~Collinear A B C [H1];
    assume seg B A === seg B C [H2];
    thus  angle B C A  === angle C A B  
  
    proof
  [...] 


Here's another example where the first line with a reported error is fine, and the real error occurs later: 

        cases;
        suppose G = A;
        qed by -;
  ::            #1
  :: 1: inference error
        suppose G = C;
        qed by -;
  ::            #1
        suppose ~(G = A) /\ ~(G = C) [AGCdistinct];
          Collinear A G C [AGCcol] by h_line, BGN, Collinear_DEF;
          G IN open (A,C) \/ C IN open (G,A) \/ A IN open (C,G) by Distinct, AGCdistinct, -, B3';
          cases by -;
          suppose G IN open (A,C) [AGC];
          qed by -;
  ::              #1
          suppose C IN open (G,A) [GCA];
          qed by -;
  ::              #1
          suppose A IN open (C,G) [CAG];
          qed by -;
  ::              #1#9
  :: 9: syntax error mizar
        qed by -;
      end

 The #1 inference error are all correct, as the proofs is the various cases have not yet been coded up.  But the #9 error occurs on a line with no error.  The problem is in the line below it, which should be `end' and not `qed'.  When we fix this, the #9 error goes away:

      cases;
      suppose G = A;
      qed by -;
  ::          #1
  :: 1: inference error
      suppose G = C;
      qed by -;
  ::          #1
      suppose ~(G = A) /\ ~(G = C) [AGCdistinct];
        Collinear A G C [AGCcol] by h_line, BGN, Collinear_DEF;
        G IN open (A,C) \/ C IN open (G,A) \/ A IN open (C,G) by Distinct, AGCdistinct, -, B3';
        cases by -;
        suppose G IN open (A,C) [AGC];
        qed by -;
  ::            #1
        suppose C IN open (G,A) [GCA];
        qed by -;
  ::            #1
        suppose A IN open (C,G) [CAG];
        qed by -;
  ::            #1
      end;
    end

Here's an example of the error being reported on a line later than the error:

        D,O',F cong A,O,C by H1, H2, -, SAS_THM:
        seg D F === seg A C by -, TriangleCong_DEF;
  ::                                              #9
  :: 9: syntax error mizar

The problem is the : on the first line, which should be a ;.  There is no other error here.



#4  unknown label
often means that you mis-typed one of the results in the by list.  You can also earn a #4 error message by misplacing the "by":

      A,D,M cong B,D,M by [ADMcong] ADMncol, Dexists, -, ADM, AngleSymmetry_THM, SAS_THM;
  ::                                                                                    #4
  :: 4: unknown label

Placing the "by" after the label gets rid of #4 error message:

    A,D,M ≅ B,D,M     [ADMcong] by ADMncol, Dexists, -, ADM, AngleSymmetry_THM, SAS_THM;


#8 syntax or type error hol

often means that e.g. a function has the wong number of arguments, or
the `by' is missing, but sometimes HOL Light expertise is needed.  You
can not e.g. define (by `let') the letter `o' as a variable, because
it already means the composition operator.  Evaluating
type_of `o`;;
tells you the hol_type of `o' is 
  `:(?143901->?143903)->(?143902->?143901)->?143902->?143903`
meaning that `o' is a function taking two selfmaps and returning the
composition.  You can see that `o' is infix operator by evaluting 
infixes();;
which gives all the infix operators plus precedence info, including
("o", (26, "right"))

#9 syntax error mizar
might mean that there's a colon (:) instead of a semicolon (;) at the
end of the line, or a ;;, or there is no ; at the end of the line,
there is a blank between two commas in the `by' list. i.e.
statement [label] by X1, X2, , X3, X4;
or that there are two occurrences of `by' on the line, as in 
      ray D C = ray D G [rDCrDG] by by DCG, IntervalRay_THM;

   Exception: Failure "lex1".
may means you have a bad character, perhaps obtained by pasting from a
pdf file, where you can the fancy quote (’) which HOL Light will not
parse, and you must replace it by the quote (').  


Use `thm' in miz3 for a theorem/proof.  The style used here is

let CarefullyChosenName_THM = thm `;
  let *;
  assume *;
  thus *

  proof

  qed     by *;
`;;

Begin with `let' variable bindings, `assume' assumptions, then state
the theorem with `thus', then give the proof beginning with `proof',
and end the proof with `qed' or `end'.  Notice that the `thus' and
`proof' statement do not end in a semicolon (;).  

The miz3 comment symbol in a `thm' body is a double colon (::).
Outside a `thm' body, use the Hol Light (* ... *) comment convention.

There are exactly two occurrences of backquote (`) in the `thm' body.
You can not have a other backquotes, even a ` commented out with ::.

If you ever accidentally paste miz3 code with e.g. a misplaced
backquote (`), into the miz3 window (or Emacs shell), type C-c to get
miz3 to forget about it (C-c C-c in an Emacs shell).  You can see
there's a bad backquote when miz3 gives you the error message
containing "Parse error".


          Exception: Failure "term_of_now".
This error occurs when ???