Bill, Michael, and all,
Let me second Michael's comments right from the start. He has expressed
most gracefully much of what I thought needed to be said.
On Tue, Aug 28, 2012 at 11:11 PM, Bill Richter <
rich...@math.northwestern.edu> wrote:
> 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.
>
For highly motivated students this may work at least most of the time. But
if the student is not so motivated, or just in a hurry, he or she is very
likely to move on immediately upon finding a solution. In learning
situations I certainly would want to be able to control the power level of
a proof assistant.
>
> 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.
>
The negative sound of the word "shackled" may be coloring the discussion.
Bill, you seem to not like the system to be limited, and you have reasons
for that. Others of us don't think that more power in the prover is
necessarily better in learning situations, but that doesn't mean one
approach is always right and the other always wrong.
What I myself would wish for in a learning situation would be "tunability"
of the proof assistant to help match it with the skill set of the students.
It seems easier to motivate students to develop their skills if the proof
assistant functions basically as a checker. I do see your point that maybe
it's not bad to guess at a step sometimes. Hopefully someday we can test
these questions empirically.
Beeson's system is interesting in that it gives hints and tailors the hints
to a level appropriate to the student's skills. So a low-level hint could
mention applying commutativity, where a higher-level hint would be to
regroup terms, a higher-level operation.
Cheers,
Cris
>
> 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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
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
