I think we should teach rigorous axiomatic geometry in high school with the aid of formal proof checkers like HOL Light, promoted by Tom Hales's Notices article. I think HOL Light needs better documentation before this is possible, and maybe new code, and I'll work on it. I need help porting my 1500 lines of Tarski geometry axiom Mizar code http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar to HOL Light Light. Details:
I wrote a paper (for my 13yo son, who read it carefully) on Hilbert's axioms http://www.math.northwestern.edu/~richter/hilbert.pdf as a bridge between Moise & Venema's rigorous geometry texts and Hartshorne's exciting but not-too-rigorous Euclid/Hilbert book. But to make rigorous axiomatic geometry a possibility in high school, I think we need to tie it into the formal proof revolution, with the spin that kids will learn computer programming skills that will help them get jobs in the new field of formally checking software. I built an old version 3.09 of HOL Light (I failed to build the newest with camlp5) and was completely bufuddled by John Harrison's 1000 pages of dox (tutorial & reference manual). How do a write down a list of axioms and get HOL to check my axiomatic proofs? A big part of the dox problem, I believe, is explained in John's thesis, which is about proving theorems in the real line with the aim of formally proving mathematical theorems needed to show the correctness of floating point computer processors. That's a long way from axiomatic geometry proofs. I'm certainly prepared to like HOL Light, which is based on ML, a Scheme-like language. I'm a pretty good Scheme programmer, and coached my son to write a nice Racket Sudoku solver on http://schemecookbook.org/Cookbook/SudokuSolver. So I switched to Mizar (which Tom's paper cites), which boasts of it's bad dox, and sorta figured it out, and wrote 1500 lines of Mizar code trying to prove Hilbert's geometry axioms from Tarski's. I more or less coded up Julien Narboux's proofs which he explains in the form of Coq code in http://dpt-info.u-strasbg.fr/~narboux/tarski.html My first step is port my code to HOL. I tried to use the various Mizar modes, but I couldn't run any of them in HOL 3.09, and I also couldn't understand how to write up such proofs. I think I made improvements to Julien's exposition, and my Mizar code is much more readable than his Coq code, and also more readable than the JHilbert code written by wikiproofs http://www.wikiproofs.de/w/index.php?title=Interface:Tarski%27s_geometry_axioms where I first learned how to use Tarski's axioms. I believe that Julien was porting proofs from the 1983 book Metamathematische Methoden in der Geometrie by W. Schwabhäuser, W Szmielew, and A. Tarski, and he got as far as Gupta's amazing proof of (more or less) Hilbert's axiom I1 that two points determine a line. It's amazing how weak Tarski's axioms are! There's no good Mizar documentation, but there are a number of pdf files with examples, and that sufficed for me. There seems to be no way of saying `` let's derive consequences of these axioms.'' So I would have liked to say, let S be a model of Tarski's axioms, i.e. a set S with betweenness and equidistance relations satisfying these 9 axioms. I think in Mizar you can only do that if you first show that a model of the axioms actually exist. And of course R^2 is a model, but that would take work to show, and I'd have to learn the Mizar of the real line, and I didn't do it. Instead I stumbled on the odd solution of making the axioms into theorems, and then I cite these axiom-theorems in my proofs. It's an OK solution if one starts on line 200 (my first actual proof) and only looks upward to find the statement of the axioms. Mizar has a particularly annoying feature of not allowing TABs or the symbols for implies etc which Isabelle/Isar (which I never built or understood) uses. So I wrote some emacs code .mizar-isar.el which gets around this. Now I write up my Mizar code in Isar fashion, using the forbidden symbols ⇒ ¬ ∨ ∧ ≡ ∀ ∃ ⇔ and not worrying about TABs, and then run my function isar->mizar which copies this file to joe.miz and rewrites it so Mizar will compile it. I also bound the forbidden symbols to keys for easy typing. -- Best, Bill ------------------------------------------------------------------------------ For Developers, A Lot Can Happen In A Second. Boundary is the first to Know...and Tell You. Monitor Your Applications in Ultra-Fine Resolution. Try it FREE! http://p.sf.net/sfu/Boundary-d2dvs2 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
