18 Jun 2012 07:59

## Re: rigorous axiomatic geometry proof in HOL Light

```I solved two problems in my in-progress Hilbert geometry formalization
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar

Math-symbols) I wrote some simple Emacs Lisp code to turn math symbols
⇒, ⇔, ¬, ∨, ∧, ∀, ∃, ⊂, ∈, ∪, ∩ and ∅.
into their HOL Light versions
==>, <=>, ~, \/, /\, !, ?, SUBSET, IN, UNION, INTER and {}
and vice versa.  I have a low level system for running HOL Light using
this emacs code explained in my tar file above.  I'm happy with it.  I
find the math symbols to be necessary to read my own code once the
proofs get complicated enough, and also I'm writing my code by pasting
in fragments copied from the pdf file of my Hilbert paper, so I have
to do something with the math symbols anyway.

I'd be interested if someone looked at the two versions of my code
(straight HOL Light and enriched with math symbols) and tells me which
one they think is more human readable.  I don't understand why ocaml,
HOL Light or miz3 can't perform the translation (from ∅ to {} e.g.).
I know John said there were Unicode issues he didn't want to deal
with.  The biconditional symbol ⇔ is ASCII char 8660, and I can
believe that having to deal with these huge ASCII char would be a
problem.  But if it's just a small number of fancy chars, it seems
they could be pre-processed, as I do in my Emacs code .

Emacs Shell) Pasting miz3 code into an xterm window has the problem
that xterm only remembers about half of my file now, so I can't scroll
up to see if I had any errors at the beginning.  So instead I create a
shell in Emacs by M-x shell and run ocaml/HOL Light/miz3 in the Emacs
shell.  I can now view my entire file, as I expected, but there's an
unexpected bonus: the miz3 output (with #s) comes at the end, and
```