Freek, I realized that my new position is that think I I don't agree with
Michael, who I believe was saying that miz3 only behaves in a Mizar-like
fashion because limitations you & John imposed on miz3 and the weakness of
MESON. If I misquoted Michael, I apologize. My new position is that miz3 is
Mizar-like enough for me no matter how powerful miz3 and MESON are. Even if
miz3 could quickly prove all my theorems if I asked it too, I can still write
up what I call readable proofs, and miz3 will only try to justify my proofs.
Miz3 won't on its own steam go prove the theorem.
>If the user only uses miz3, as I do, to justify statements that
>appear obvious to them, then I think miz3 is fine.
Sure. But do you remember that time when you thought that miz3 had
accepted a "wrong" proof, when in fact it had just been clever?
(Something about a line through two points when it hadn't been
given the distinctness of the points?) So even accidentally it
might be taking shortcuts that for your own understanding shouldn't
have been taken.
Good point, and let's take another look at your excellent explanation, which
I'll exposit with this code:
horizon := 0;;
new_type("point",0);;
new_constant("Line",`:point_set->bool`);;
let I1 = new_axiom
`!A B. ~(A = B) ==> ?! l. Line l /\ A IN l /\ B IN l`;;
MESON[I1] `~(B = C) ==> ?p. Line p /\ A IN p /\ B IN p`;;
let BillBlunder_THM = thm `;
let A B C be point;
assume ~(B = C) [H1];
thus ?p. Line p /\ A IN p /\ B IN p
by H1, I1`;;
The MESON "solved at" numbers are 2318 and 2319, essentially the same, and I
would not consider this to be a Mizar-like proof, as the reasoning is, for me,
too difficult. Your explanation, which I accept, is that MESON performed the
reasoning in this miz3 proof with MESON "solved at" number 99:
let FreekExplainsMESONReasoning_THM = thm `;
let A B C be point;
assume ~(B = C) [H1];
thus ?p. Line p /\ A IN p /\ B IN p
proof
cases;
suppose A = B [AB];
?p. Line p /\ A IN p /\ C IN p by -, H1, I1;
qed by -, AB;
suppose ~(A = B) [notAB];
qed by -, I1;
end`;;
This example shows that I'm capable of fooling myself into thinking I have
simple Mizar-like proofs, when I'm actually making secret leaps like in
BillBlunder_THM, because I actually coded up a proof like that.
But such is life. I suppose someone might want a proof assistant that is so
weak that if it verifies a proof, then we'll know the reasoning was indeed
blitheringly obvious. I did think that miz3 was such a weak proof assistant,
and it was a jolt to realize how powerful miz3 actually is. But I don't need
such a weak proof assistant. If I'm so dumb that I write up hard proofs and
think they're easy proofs, maybe I'm not a good mathematician! And if my
students code up proofs with leaps in them that I'm too lazy or stupid to spot,
maybe I'm a bad teacher. It's the road to ruin to want our technology to be so
good that we don't have to be smart.
--
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
