John, thanks for the advice and new code! I'll try it tonight on the latest hol_light subversion, as my sysadmin installed svn and:
svn checkout http://hol-light.googlecode.com/svn/trunk/ hol_light [...] Checked out revision 135. (poisson)richter> du -s hol_light/ 47772 hol_light/ I see you added Freek's miz3, and hol.ml still reads let hol_version = "2.20++";; (poisson)richter> tar zcvf HOL-L135.tar.gz hol_light (poisson)richter> du -s HOL-L135.tar.gz 7372 HOL-L135.tar.gz I trust these numbers look all right. I'm really happy to be working with your on this Tarski geometry hol_light/miz3 project. Yes, I didn't give an axiomatic proof of your equation, and such an axiomatic proof sounds pretty dismal. I wouldn't know where to start. Rob, that's very cool that John's equation comes from quaternions! I'll look at your Wiki Lagrange's_four-square_theorem link. Freek, thanks for jumping in! And thanks for writing miz3! I took your advice (and Makarius's) and tried Isabelle. You should try it, as it's just one download, and has a nice integrated editor jedit. But I couldn't understand Isabelle proofs, so miz3 looks great. Josef, that's interesting that you vampired my code. Your Mizar formalization (joe.miz). The 5 theorems that Vampire could not solve were the longer ones, like Gupta, I1part1, etc . Cool. I think that's a tribute to the Coq skill of Julien's Narboux, from whom I learned the proof of Gupta. mew (woodcock), all mathematicians accept is that math is nothing but corollaries of the ZFC set theory axioms in a model of ZFC, which is presumed to exist. That is, we use the set theory axioms on sets that we assume actually exist. In practice, mathematicians don't understand ZFC very well, and Halmos's book Naive Set Theory explains how hard it is to get the real line out of ZFC. I'm sure John understands ZFC better than I do, and I assume he coded the ZFC axioms in some first order logic way in HOL LIGHT. And I assert that no mathematician would quarrel with John's HOL LIGHT formulation of ZFC. Now the ZFC model proofs that mathematicians create are much nicer to read than FOL proofs, but set theorists proved that such ZFC FOL proofs must exist. The theorem (I forget what it's called) is that if a theorem is true in every model of a first order theory, then there exists an axiomatic FOL proof of the theorem. -- 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
