On Thu, May 24, 2012 at 3:47 AM, "Mark" <[email protected]> wrote:
> 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;
>
Doing interactive formal proofs such as proofs of "real theorems" (like,
say, the Pythagorean theorem in geometry) is not what I am focusing on at
the moment.
> b) getting students to use theorem provers as advanced calculators;
>
OK, you're definitely getting warmer, especially if you mean "symbolic math
calculators". I don't care for the "calculator" label though, and it does
not seem justified to me. Consider for example axioms for real numbers that
include commutativity, associativity, and distributivity of + and *. Even
the rather primitive inference steps currently supported by Prooftoys are
at a level or two above direct application of such axioms. And
textbook-level expansion (and simplification) of (2x + 3) * (1 - x) is a
level or two above that. Yet in a sense it is still using a theorem prover
as a sort of calculator.
Do you see any particular distinction between the concept of a "symbolic
calculator" and a proof assistant? Perhaps the calculator part would only
uses proof procedures guaranteed to terminate quickly. I'm concerned about
(gasp!) the marketing aspect of using the phrase "symbolic calculator".
>From what I have read about Mizar, it seems to only prove steps internally
that it can do quickly; yet I would be sorry to see it called a calculator.
> 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)?
>
This to me is a worthy thought that interests me quite a bit. But so far my
greatest interest is in finding ways to drive adoption of proof
assistant-type tools. Improved usability I expect will help quite a bit.
But frankly I'd like to see these tools turn into a habit for doing math,
perhaps a bit like spreadsheets are for people in finance. And I happen to
think that improved tools -- and habits(!) -- can drive increased use of
mathematical reasoning, for example in my own field of software
development. But that of course is a huge digression in itself ...
So on to your other fine questions:
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.
>
Well yes, undergrad students as well, but hopefully not _instead_ of high
school students, meaning up to about 12th grade, eh? I hope that is also
what Freek means by "high school".
I think my own kids did a bit of proof in their high school geometry
classes, but I'm sure it was not much. I fear that as you suggest, there is
very little proof done in high schools in the U.S., but I am not informed
on this.
So what am I really trying to do right now?
Some of you may be aware of the rather popular free, online Khan
Academy<http://khanacademy.org/>service. It started with math
education and is strong in that area. In
particular they have a sophisticated system for practice in solving math
problems. Their system analyzes a student's results in practice sessions to
try to move him or her ahead at the most effective rate and to determine
what he or she can best practice next.
They have no decent way however to tell what steps the student is doing
when a problem might be done in steps. I have created a tiny
proof-of-concept demo for them, which you should be able to see on
this experimental
web
page<http://sandcastle.khanacademy.org/media/castles/crisperdue:cris-testing/exercises/expression_expansion.html>.
Click on an expression to be expanded or simplified, and select a rule to
apply for one step of the problem. Repeat as needed. Should work in modern
Firefox, Chrome, or Safari browsers.
This way the system can see and analyze the student's work step by step in
"real time", and the tool may help guide the student as well. Of course I'm
not trying to limit use of proof to such simplistic examples.
This email is getting more than long enough, so I'll quit for now.
Best regards,
Cris
>
> 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
