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
