Cris, the axiom of choice is essential in much of modern math, and I'm guessing that's John's reason.
Rob, that was a very interesting post, which I can't do justice too. I would be very interested if you say anything about Vladimir V's Coq work. Your Topology paper looks very cool, and I'll try to read it and ask you how to port it to HOL Light. Did you say that ProofPower has Isabelle-type fonts (foralls and exists and cups and caps etc.)? I have those myself in HOL-Light, and John approved of my Emacs pre-processor style, as you'll see if you read my code, now with a very nice proof of Euclid's Prop I.7, of which Hartshorne gave an incomplete proof http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz EuclidProp7_THM : thm = |- !A B C D a. ~(A = B) ==> Line a /\ A IN a /\ B IN a ==> ~(C = D) /\ C NOTIN a /\ D NOTIN a /\ C,D same_side a ==> seg A C === seg A D ==> ~(seg B C === seg B D) If you can't read Mizar proofs, maybe I'm your man. I'm sure you can read the miz3 proofs I coded for your proof of Los's Logic problem. I can't believe you'd have any trouble reading my miz3 Hilbert code above. I heartily dislike the Mizar type system and the Mizar vocabulary biz. Perhaps we're not talking about the same thing. To understand Mizar or miz3 well enough to code it yourself is very different from merely being able to read proofs others wrote. Thanks for clarifying HOL4, ZFC vs ZC, and I have to set this off, it sounds so cool: Instead of HOL, we should call it polymorphic typed set theory The overwhelming advantage of readable proofs is that CS folks and mathematicians can work together on formal proofs. Isn't that a great team? I certainly think so, because the CS folks are the ones who are good at computers. I think John answers your questions about "tools that can outstrip human capability" in the interactive chapter of his purple book. Basically, I think, he says that neither of the two approaches (get the computer to do it, or write up the proof in full yourself) is that powerful, so they should be mixed together. As John thanks you (and Michael etc) for help, maybe you make a reply here. -- 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
