JH> This reminds me of something Andrzej Trybulec said about automated JH> theorem provers: why should we let the machine deprive us of the JH> pleasure of proving things?
I just tried this, and it turns out that Vampire (fitting name) would fully deprive us of this pleasure in all but five theorems in Bill's article :-). Josef, I can't follow this. Can you try again? BTW thanks for the link to AI visionary John McCarthy. As I explained, it's a great pleasure to use Mizar to check my readable proofs, but it would be no pleasure if I couldn't understand what the machine was doing. Isn't that what Andrzej meant? What's Vampire? Which 5 theorems & Bill article? My geometry paper? http://www.math.northwestern.edu/~richter/hilbert.pdf While I'm here, let me handle two relevant points John (who wrote some amazing code for me!!!) made: HOL Light may be readable enough for me. ==>, /\ and \/ are much more readable to me than the Mizar implies, & and or. | I say the first requirement for a good proof assistant is for | humans to be able to code up nice readable axiomatic proofs. I think the main focus has been on raising the level of automation to the point where one can handle proofs that are not already presented in a nice axiomatic way. That's a much more interesting and ambitious goal. Maybe I was making a documentation point. In order to pull in mathematical type folks, I think that proof assistants should start out by explaining how to check some axiomatic proofs. Here's a rather long readable proof of some propositional logic result, and here's how we can use our proof assistant to speed up the proof through various automation strategies. I'd be happy to write such documentation after I understand hol_light. Maybe the problem is that axiomatic geometry gives more interesting examples than prop logic, but few folks understand Hilbert or Tarski. As a thought-experiment, imagine writing an explicit axiomatic proof of the following identity over the reals: John, that's definitely an example of poor hol_light readability, and I vastly prefer my pseudo-TeX: (x1^2 + x2^2 + x3^2 + x4^2) (y1^2 + y2^2 + y3^2 + y4^2) = (x1 y1 - x2 y2 - x3 y3 - x4 y4)^2 + (x1 y2 + x2 y1 + x3 y4 - x4 y3)^2 + (x1 y3 - x2 y4 + x3 y1 + x4 y2)^2 + (x1 y4 + x2 y3 - x3 y2 + x4 y1)^2 The thought of being forced to do it by hand is pretty dismal, at least to me. John, I proved it!!! On both sides we get the 16 x_i^2 y_j^2 terms. That's it for the LHS, but the RHS is twice the sum of 4 * 6 = 24 terms of the sort xi xj ys yt for i != j and s != t. With this in mind, add the 1st two squared terms, and then add the last two squared terms. See if you see the pattern. I'll skip a screen and do it: The four squares on the RHS group in pairs. Ignoring the x_i^2 y_j^2 terms and dividing by 2, (x1 y1 - x2 y2 - x3 y3 - x4 y4)^2 + (x1 y2 + x2 y1 + x3 y4 - x4 y3)^2 + "=" (x1 x3 + x2 x4)(y2 y4 - y1 y3) + (x2 x3 - x1 y4)(y14 + y2 y3) (x1 y3 - x2 y4 + x3 y1 + x4 y2)^2 + (x1 y4 + x2 y3 - x3 y2 + x4 y1)^2 "=" (x1 x3 + x2 x4)(y1 y3 - y2 y4) + (x1 x4 - x2 x3)(y1 y4 + y2 y3) Those are amazing equations, and adding them we get 0, and this proves your equation is true. Wow! How did anyone think your equation up? John, I'm not real sure what you'd mean by an axiomatic proof here. But it might be a good in the manual to explain how someone could prove this by hand, and then how to automate it. And this brings us to Andrzej's point: Not knowing about my intermediate step here would definitely have deprived me of pleasure. -- 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
