Hi, Cris --
Your educational project sounds very interesting!
> They have no decent way however to tell what steps the student is doing when
> a problem might be done in steps.
Are you familiar with Michael Beeson's MathXpert (formerly MathPert)?
It is a powerful educational system for learning high school and first-year
university mathematics (including basic real algebra, trigonometry, and what in
the US is called `single variable calculus'), and uses theorem proving in the
background to check students' steps, verifying side-conditions and so on.
Beeson spent a lot of effort (reflected in interesting discussions in his
papers) on the system's `cognitive fidelity,' i.e., designing it to solve
problems in a way that a good student would. If memory serves, its calculus
support is based on non-standard analysis under the hood.
You can find links to papers about it on Beeson's homepage (publication #'s
28-31): http://www.michaelbeeson.com/research/papers/pubs.html
The MathXpert website is here: http://helpwithmath.com/ , and there is some
background on the ideas underlying it here: http://helpwithmath.com/about.php
Best wishes,
Grant
On 24 May 2012, at 17:20, Cris Perdue wrote:
>
>
> 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
> 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.
> 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
------------------------------------------------------------------------------
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
