Thanks for the reply, John (and others)! Let me make a quick response. I mostly wrote my Mizar code to cite in my geometry paper http://www.math.northwestern.edu/~richter/hilbert.pdf If other folks have already done a better job, that's great, I should just cite their code instead of mine. I haven't found their code yet. If you think Mizar is the right language for axiomatic geometry proofs, I should use it, unless I can upgrade to Isabelle instead.
But I don't like that plan, and I think you don't either. I think we think that HOL can easily be tweaked to give axiomatic geometry proofs that are just as readable as my Mizar proofs. How do we get started working on this? I can't yet use any mizar mode in HOL Light, and maybe because I can only build an old version 3.09. Your article sounded very interesting, but I couldn't find it: Szczerba The use of Mizar in a course in foundations of geometry Your geometry links don't seem to jibe well with my paper above. As Roger & Phil are posting about Hilbert & Euclid, let me expand: I've barely looked at Hilbert's book FoG. Hilbert does a better job with angle addition than Greenberg. It could be that FoG has gaps. I've learned almost all my Hilbert from books by Jahren, Greenberg & Hartshorne. My paper explains the following clearly: Euclid could not rigorously prove anything involving angle addition. Euclid's errors can be fixed Hilbert's betweenness axioms. Euclid could not rigorously prove the triangle sum theorem (sum angles = 180). I do, and I actually think I have the simplest rigorous proof, as the other rigorous proof I've seen in Forder first prove the non-Euclidean version (sum angles <= 180) which is a lot harder. Phil, I also explain (following Moise's rigorous book) how to handle the 3-dim part. Basically, for all the 2-dim stuff you have to say "in a plane" and in the 3-dim part you use the planar stuff. Euclid's book XI is a fantastic treatment of solid geometry, and Moise simplifies some of Euclid's proofs. There's an interesting AI angle: can robots visualize 3-dim space? Well, by Hilbert's axioms and the Goedel's completeness theorem, they can know everything we know about points, lines & planes in 3-space! that's another reason to learn rigorous axiomatic geometry proofs. This is a nice example: even the question of whether a proof is actually faulty or just leaves a huge "pedagogical gap" that the original author was easily capable of filling is itself ambiguous. Thanks. In my case, I know that none of the folks who published that there was a combinatorial proof of the two Lambda algebra results actually knew a proof. Interesting to hear you say that, since many mathematicians seem quite blase' about correctness issues, even with the huge proofs that few people could claim to follow in detail. That's excellent, John. I think there's two disturbing factors: 1)The rewards in math are for getting credit for proving a cool theorem, and not for writing up nice proofs that others can read. 2) Mathematicians prove theorems as a community, so no one person understands the whole proof. It's amazing that communities can work together like this. But it's a rejection of the Enlightenment value ``Understanding is Power.'' Understanding more or less means understanding mathematical proofs. -- Best, Bill ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
