Hi Cris,
Thanks for the enthusiastic endorsement! I know what you mean about years
of training instead of months of training. I was erring on the side of
understatement rather than overstatement!
I'm not sure if I've got the webpage working properly on the Khan Academy
website. What is supposed to happen on the page? I haven't taken a good
look at MathXpert yet, but I should defnitely do that.
Thanks very much for you offer of help. What I want to do first is a
classic "LCF-style" interactive theorem prover in an ML toplevel, that will
act as the logical brain of the system. But after that, to get serious
adoption, there will be a tonne of supporting stuff that needs doing,
including user interfaces, webpages, training manuals etc, and any help here
would be extremely useful. Also, just getting input from people about what
the requirements should be is always useful. But this is all a few years
away - it will be several months before I can even resume work on it.
In terms of design, I think the way to go is, as you suggest, to look at
proofs of recognisable theorems in mathematics. It should be possible to
get step-for-step correspondence between textbook proofs and theorem prover
proofs. Undergraduage textbooks mix English prose with lines of
mathematical notation, but it is straightforward to extract out identifiable
proof steps and turn this into a rigorous symbolic pen-and-paper proof, with
steps at the same level as the original. What I am aiming at is a theorem
prover that makes formalising such pen-and-paper proofs quick and trivial.
It should also be possible to restrict the kinds of jumps in reasoning that
the user is allowed to do in one step, so that the same system can be suited
to both formalising undergraduate textbooks and policing much more basic
high school proofs. I don't see why professional mathematicians and school
children can't be using the same system. I certainly think that theorem
provers will never get widely adopted until such a system exists.
Actually, a very interesting exercise was Freek's challenge at ICMS 2006,
where he asked expert users of various theorem provers, including HOL Light,
Mizar, Coq and Isabelle/HOL Isar, to formalise a classic textbook proof.
http://www.cs.ru.nl/~freek/demos/index.html
Regards,
Mark.
on 7/7/12 12:59 AM, Cris Perdue <c...@perdues.com> wrote:
> Mark and all,
>
> Yay! That's a beautiful description of key characteristics of tools that I
> believe will have great benefit and impact when they arrive on the scene.
> Reading through it a couple more times, I'm not sure there is any point
> where I do not heartily agree. This is something I want to contribute to
> with my software skills and enthusiasm for logic. It is also the
motivation
> behind the Prooftoys (http://prooftoys.org/) work to date, and it is a
> vision I am prepared to contribute to as much as I am able in the future.
I
> would like to call out at least one point:
>
> "not require months of training"
>
> This is an understatement. My too-many years of experience with software
> technology are hollering deafeningly that making adoption drop-dead easy
is
> the real target. OK, "Proof is not that simple" you say, and of course you
> know what you are talking about. Rather than harangue you all further on
> the subject, I'd like to point you to a couple of examples.
>
> Using Prooftoys I have made a proof of concept demo that works in the Khan
> Academy math exercise framework, at
>
>
http://sandcastle.khanacademy.org/media/castles/crisperdue:cris-testing/exer
> cises/expression_expansion.html
> .
> Or get a trial version of Michael Beeson's MathXpert and do just about
> anything. MathXpert steps are all mathematically correct, and it manages
> the "side conditions" behind the scenes unless they "block" a step or you
> go out of your way to look at them. And I would say a bright high school
> student could pick it up pretty darned fast if he or she actually tries
it.
>
> Of course I'm talking about adoption by individual users, not be schools
or
> teachers, which is vastly different and in the end will only be possible
> following much adoption by individuals.
>
> One serious question is whether it is possible to work up by baby steps
> from there to more serious sorts of proofs so adopters can easily work up
> from there to "actual proofs", fuller use of the logic, and ability to
> express classic styles of informal reasoning (or in Mark's words "proof on
> paper"). I absolutely think it is possible, but definitely an issue.
> Clearly a lot more could be said here.
>
> Another approach might be to start immediately with proofs of recognizable
> theorems, in the spirit of Euclid's Elements, but formal of course and not
> necessarily in geometry. I do not have a lot of thoughts right now on what
> success may be possible this way, but am following Bill Richter's
> experiences with much interest.
>
> Reasoning it seems to me is such a valuable tool, and computers are so
well
> suited to supporting it, that hopefully much more of the potential value
> here can start to be realized in the reasonably near future. Certainly it
> seems under-appreciated and underutilized in my own field of software.
>
> In any event I'm very interested in contributing to such an effort as
> effectively possible, with software development or user interface skills,
> with enthusiasm for logic, or in other ways, so please feel free to
> contact me on anything related to any of this.
>
> Best regards,
> Cris
>
> On Fri, Jul 6, 2012 at 9:53 AM, "Mark" <m...@proof-technologies.com>
wrote:
>
>> Hi Bill,
>>
>> I understand exactly what you are looking for (or at least I think I do!)
> -
>> a theorem prover with very clearly defined functionality, that automates
>> what is "trivial" and does not automate what is not "trivial", and that
is
>> easy to use, caters for all the classic styles of doing (symbolic) proof
> on
>> paper and does not require months of training. And if this system is
also
>> a
>> "serious" system involved in the formalisation of mathematics, and is
>> highly
>> trustworthy, then all the better. You see such a system as being an
>> excellent way of teaching students how to do proof.
>>
>> As you say, Mizar and miz3 (and don't forget Isar) perhaps come about the
>> closest of any current systems to what you want. I've had in mind for
> many
>> years a design of a system that does exactly what you want, but have been
>> too busy with other stuff to develop this up till now. I suppose this
>> doesn't really help you until it's been implemented, but I just wanted to
>> tell you that!
>>
>> I suppose a problem with using existing systems is that they are trying
to
>> do something different - to enable proofs to be proved with minimal
amount
>> of user effort. Sometimes the approach they use to achieving this means
>> that they come close to your goals, but they will never be perfect for
> what
>> you want.
>>
>> By the way, "malicious" proofs are not proofs that use a theorem prover's
>> automatic facilities when they are not intended to be used. Malicious
>> proofs are proofs that deliberately take advantage of unsoundness (or
> other
>> trustworthiness issues) in the theorem prover, to prove a fallacy, or to
>> appear to prove a fallacy.
>>
>> Mark.
>>
>>
>> on 6/7/12 7:45 AM, Bill Richter <rich...@math.northwestern.edu> wrote:
>>
>> > My question is: What kind of proof is miz3 saying I have? Recall that
>> > my long-term purpose is to teach a rigorous axiomatic high school
>> > Geometry course. There must be powerful theorem provers that could
>> > prove every result in the course! Josef got Vampire to prove most of
>> > my Tarski miz3 results. So I'd like to know that miz3 isn't powerful
>> > enough to make it useless for teaching Geometry! I think miz3 is just
>> > about right, from my experience of 2350 lines of Hilbert axiomatic
>> > code and 985 lines of Tarski code, but I'll never be sure until I know
>> > what miz3 calls a proof. Part of the problem is that there's no
>> > documentation for exactly what a Mizar proof is. Again, from my
>> > original Tarski code experience, I think Mizar is about the right
>> > level of power. But I don't know, and can't explain it in my paper.
>> >
>> > ....
>> >
>> > Here's my hazy idea. I more or less know what an FOL proof is, and I
>> > think writing them down is tedious, and we'd like a proof assistant to
>> > automate the tedious details (substituting variables etc) , so we're
>> > left with the interesting part of the FOL proof. I think this is what
>> > Mizar, John's Mizar-like FOL, and miz3 all do. But I'd like to know
>> > for sure, and more precisely, exactly what automation they do.
>> >
>> > It's never happened that when I ``intentionally'' wrote up a miz3
>> > proof, that miz3 proved the theorems before I thought I had completed
>> > the proof. That's what I want. But once I goofed in my miz3 proof,
>> > miz3 approved a proof that I didn't think was a proof. Freek
>> > explained that MESON is quite powerful, and explained how MESON proved
>> > my result. So as long as I don't goof like that, I'm OK. But could
>> > my students exploit the power of MESON to hand in miz3 proofs that I
>> > wouldn't call proofs? I know issues like this get discussed here,
>> > maybe it's called `malicious' proofs. I'm not really worried about
>> > malice, and I'd be thrilled to have any students, but the teacher
>> > ought to know what the proof assistant will accept as a proof.
>>
>>
>>
>
----------------------------------------------------------------------------
> --
>> 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
>> hol-info@lists.sourceforge.net
>> 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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
