Hi Cris, I agree with you and Freek that it's a good idea to concentrate on "high school math".
Can I ask, which of the following 3 are you specifically talking about: a) getting students to use theorem provers to perform interactive formal proofs; b) getting students to use theorem provers as advanced calculators; c) concentrating on "high school math" as a way of improving theorem prover usability (without any necessary intention of actually getting high school students to use this)? Also can I ask are you specifically talking about high school students, or perhaps undergrad students instead/as well? If you are looking to support actual high school students, which countries are you thinking of? Do they even still do proof at high school in the USA, for example? It seems that it's almost been banished from the cirriculum in the UK, I found out at an education conference a few years ago. I don't know about other countries. Of course this sort of thing would still be very useful to undergrad courses around the world. Mark. on 24/5/12 1:56 AM, Cris Perdue <[email protected]> wrote: > Reading Freek Wiedijk's paper "Formal Proofs: Getting > Started<http://www.ams.org/notices/200811/tx081101408p.pdf>" > has been very interesting for me, but raised a question that seems > important to some of my goals, and it seems to me that he and other members > of this group are probably a great resource that can help. > > Please bear with me through a bit of background. My ongoing personal > project is the Prooftoys visual proof assistant (http://prooftoys.org/). > Its biggest goal from the start has been to help popularize use of proof > assistants by being easy to try out, learn and use. It is a Web application > and immediately available through its graphical user interface to anyone > visiting a suitable web page. > > As I have continued working on it and learned more about the field, I have > come increasingly to feel that application to high school-level math and > math problems may be the best short-term opportunity to advance this > particular cause. (In fact I have taken some concrete steps in this > direction.) Good proof assistants can do a lot of math these days, so the > chances have looked very good to me, though of course there will be many > details to work out in functionality, usability, and other areas. > > But Freek's paper says: > > However, currently steps in a proof that even a high school student can > easily take without much thought often take many minutes to formalize. This > lack of automation of “high school mathematics” is the most important > reason why formalization currently still is a subject for a small group of > computer scientists, instead of it having been discovered by all > mathematicians. > > This could be a genuine obstacle to what I have in mind! Now I am a > relative newcomer to proof assistant software, and it is significant work > for me to implement things like rewriting rules to take care of common > simplifications and such, but I have tended to assume it was just me. > > So I am asking you to help me understand how true Freek's statement may be. > Can some of you give examples of steps that would tend to be obvious to > high school students but not easily handled by a proof assistant? Or steps > that could reasonably appear in examples in a high school textbook, but be > not simple for a proof assistant? (I'm thinking particularly of algebra, > trigonometry, maybe even up to calculus, but I do not understand the issues > of formalizing geometry well enough to absorb comments about assisting with > geometry problems. And I'm not really thinking of students who have > aptitude as potential professional mathematicians ... ) > > Any guidance or thoughts in this area will be very greatly appreciated. > > Cheers, > Cris > > > > ---------------------------------------- > > ---------------------------------------------------------------------------- > -- > 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 > > > ------------------------------------------------------------------------------ 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
