X

#### Xah Lee

American Mathematical Society published a series of articles on formal

proofs in 2008 November. See: http://www.ams.org/notices/200811/ The

articles are:

â€¢ Formal Proof by Thomas Hales

â€¢ Formal Proof â€” The Four-Color Theorem by Georges Gonthier

â€¢ Formal Proof â€” Theory and Practice by John Harrison

â€¢ Formal Proof â€” Getting Started by Freek Wiedijk

I read 3 of them in December (only scanned the four-color theorem

one).

It was quite a fantastically enjoyable reading.

(

For some personal notes, see: Current State Of Theorem Proving Systems

at the bottom of

â€¢ The Codification of Mathematics

http://xahlee.org/cmaci/notation/math_codify.html

)

As you may know, codification of math has been a long personal

interest. In fact, my logical analytic habit has made me unable to

read most math texts, which are full of logical errors and relies on a

â€œhumanâ€ interpretation for its soundness and clarity.

having read those intro articles from the AMS publication on current

state of the art, i decided that i'm going to learn HOL Light. (tried

to learn Coq before and the tutorial is problematic)

One of the interesting finding was that almost all theorem proving

systems are written in ML family lang, e.g. Caml, Ocaml. Of course, i

heard of Ocaml since about 1998 when i was doing Scheme. Somehow it

never impressed me from reading the functional programing FAQ. I have

always been attracted more to Haskell, perhaps only because it is

_pure_ in the sense of not allowing assignment. With that, ocaml has

been â€œjust another functional langâ€ in my mind. But now, seeing that

most theorem proving systems used in the real world are in Caml, thus

i made start to learn Ocaml now. (in fact, its root is a theorem

prover)

i wanted to add proofs as enhancement to my A Visual Dictionary Of

Special Plane Curves. Also, had ambition to write more... about

algebraic geometry and differential geometry and geometry with complex

numbers. Proofs will be major part of these type of works. I can no

longer tolerate traditional mouthy written-english proofs. They must

be codified proofs.

In this:

HOL Light Tutorial (for version 2.20)

by John Harrison

September 9, 2006,

there's this paragraph:

â€œThis fits naturally with the view, expressed for example by Dijkstra

(1976), that a programming language should be thought of first and

foremost as an algorithm-oriented system of mathematical notation, and

only secondarily as something to be run on a machine.â€

Wee! That has been my view since about 1997. The only lang that adhere

to that view i know of is Mathematica.

(lisping morons don't understand a iota of it. See:

â€¢ Is Lisp's Objects Concept Necessary?

http://xahlee.org/emacs/lisps_objects.html

â€¢ The Concepts and Confusions of Prefix, Infix, Postfix and Fully

Nested Notations

http://xahlee.org/UnixResource_dir/writ/notations.html

)

btw, anyone know the source of that Dijkstra quote?

Xah

âˆ‘ http://xahlee.org/

â˜„