Hello Grant,
On Thu, May 24, 2012 at 2:28 PM, Grant Olney Passmore <[email protected]
> wrote:
> 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.
>
Yes, I am slightly familiar with MathXpert though at this point I really
must become more familiar with it. It turns out that Michael and I are
local to each other, and at an earlier stage of Prooftoys I sent him an
email that resulted in having lunch. At that point Prooftoys did not excite
his involvement. Anyway, I was just building logic theorems and inference
rules and not especially considering high school-level mathematics. What I
have seen of MathXpert has been quite positive, and your comments certainly
reinforce that impression. It is a shame that being so far ahead of its
time has caused it to be so much overlooked.
Though I did read a little about MathXpert I was not aware of his scholarly
papers about it. Thanks much for pointing them out.
-Cris
>
> 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<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
>
>
>
------------------------------------------------------------------------------
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
