Thanks, Michael! I like what you wrote about (me and) the student with "little sophistication when it comes to writing proofs," but I can't see we're helping by shackling their proof assistant. I want people to learn how to write and understand mathematical proofs, and I think proof assistants (especially miz3) can help students learn. It worked for me! I understand Hilbert geometry a lot better after formalizing my paper. I could see this helping students at every level. Does anyone (other than Cris, who I know does) share this objective?
1. the student doesn't waste time waiting for the prover to give up on unrealistic or unprovable goals. Fast feedback is universally recognised as a good thing when using a system: having it come back fast and say "No. Make your proof better" has to be a good thing for learning how to make better proofs. Great, and that's exactly what Freek and I said earlier about why timeout is set to 1 by default in miz3. Do you agree that miz3 isn't intentionally shackled, and that John would be delighted if we figured out how to make it more powerful? 2. if the student does occasionally get the backend prover to fluke a hard result, they miss out on the pedagogically valuable exercise of actually proving that result. Doesn't the student realize they didn't prove the theorem? Shouldn't they say, that's great my PA proved the theorem (I want to have a powerful PA), and now let's see if I can prove it too. If so, they don't miss out, and I could see going for occasional flukes as a way for the student to test their intuition. Do you really want a student to be able to come back to you with that theorem due to Los, and say "Oh, I proved it by waiting for meson to finish." Well, they'd only wait a few seconds (a 20,000 solved at MESON number is quick: my code runs 15 minutes on my slow home computer). I don't know what you mean by `able'. I want to the students to know the difference between them understanding a proof and MESON proving it. If they're learning to prove theorems and write them up, they should know that by the time they get to a really tough result like Los's. Bill thought that proving it by hand was interesting and valuable, and discussed Rob Arthan's proof at length. Surely the value that Bill derived from that exercise would be just as great for students. Yeah, absolutely! I'd tell the kids what I learned from Rob, you can emulate what MESON did by calculating the possibilities, and then tell them to try a bold frontal attack of looking at 4 points, or maybe even 3. I'd want to know if any of them could replicate Rob's brilliant success. So I say if the students want to learn proofs, a good PA can really help them, but let's respect the students and let them set the timeouts. If the students don't want to learn proofs, I doubt we can force them to by shackling the PA. Maybe I'm being too idealistic. I think hand calculators are a great way for kids to learn manual arithmetic well enough to believe the distributive, associative etc laws that are so vital to understanding Algebra. A good exercise is writing 1/7 as a repeating decimal and then turning that repeating decimal back into a fraction, and then reducing it to 1/7. Well, that's a lot easier to do if you get your calculator to do some of the work. This of course hasn't been the effect so far of calculators in math classes! Many Calculus students told me that they can't do algebraic simplifications because they don't have to, their calculators will graph functions any way they type them in! BTW the great mathematician Bill Thurston just died. He wrote a very interesting article On Proof and Progress in Mathematics Bulletin of the A.M.S. 1994 http://www.ams.org/journals/bull/1994-30-02/S0273-0979-1994-00502-6/S0273-0979-1994-00502-6.pdf I posted a tribute on a topology listserve https://lists.lehigh.edu/pipermail/algtop-l/2012q3/001462.html talking about Thurston's interest in computers he showed in this article. Josef, I don't think you answered my question. But we're even, because I haven't read Piotr's article. But I will conjecture, on the basis of Michael's great post about illusions and sweet spots, that there is no good way for the PA to restrict the users to "obvious inferences." That shackling the PA in this way is a hit or miss game of setting various timeouts & limitations, which might work in a lot of cases, but there's no science to it, we're just monkeying with various numbers. I suspect it's the inelegance of this that monkeying around with the timeout & depth numbers that bothered Michael, and it bothers me now too. OK, I've made my conjecture, now I can go read Piotr :) Let me stress that I think that Mizar made a fantastic contribution, continued by John & Freek with holby/miz3, of ALLOWING us to write human readable proofs. I don't consider that Mizar made an accomplishment if they (and you & Michael say they did) tried to FORCE us to write human readable proofs. -- 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
