Phil, I'm sorry, I lost your message and just found it. What sort of granularity do you want in the proof steps?
The proofs in my Mizar code skip more steps than I'd like http://www.math.northwestern.edu/~richter/RichterTarskiMizar.tar I think the proofs are going to get massive even at the very beginning of Hilbert's geometry. Maybe Tarski's is more suitable. I think my Mizar Tarski proofs are about like my Latex Hilbert proofs http://www.math.northwestern.edu/~richter/hilbert.pdf and they're both a nice size for me. You have to remember that my sources (Hartshorne & Greenberg) are much nicer expositions than FoG. I'm generally all in favour of teaching rigorous mathematics to high-school students, getting them to use theorem provers and learning to code early. Here in the UK, we are falling ever further behind in terms of computer science at high-school level. That said, it seems that students would be faced with a huge learning curve if they were simultaneously studying a relatively poorly documented language such as Ocaml, a theorem prover such as HOL Light, and the axiomatic method. The proof assistants will just check 2-column geometry proofs. My students (right now just my 13yo son) will learn next to nothing about Ocaml or any proof assistant. So good documentation is needed, and quite likely a better interface. I always get a rush when Mizar tells me I've got a rigorous proof, and I think the kids will too. And my guess is they'll have trouble no matter which theorem prover you pick, though I'm very much interested in your thoughts on how to tackle this. I'm mostly interested in the rigorous axiomatic method, and I'm mostly using proof assistants as a selling point: you should learn math proofs to get a good job programming computers later in the new hot field of proof assistants checking software. Your project is much more ambitious programming, filling in the gaps of the first thing ever written on Hilbert's axioms, written long ago (do you have the latest edition BTW? The axioms are weaker). To go a little off the deep end, it's like the difference between listenin to the Sweet Honey and Rock version of the Beatitudes http://www.youtube.com/watch?v=NrmhRoS-XE4 and reading the Gospels in the original Greek or Aramaic. You & Jacques need real proof assistants and ML skills, but I shouldn't. -- 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
