Hi Mark,
I really do think we are excited by the same overall vision, which is
great! Shared vision I believe is probably the greatest key to building
successful collaboration.
Now come some interesting parts -- someone like me coming in with perhaps
rather different work history and from a different "technical culture", and
with limited grounding in automated deduction and formalization of math. We
may each have to (metaphorically) "speak slowly and clearly" to be
understood by others not accustomed to our way of talking. ;-)
Further comments in-line:
On Mon, Jul 9, 2012 at 2:24 AM, "Mark" <m...@proof-technologies.com> wrote:
> 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'll let people like you decide how much training it seems to take for
people to become proficient in different aspects of proof assistants. What
I was talking about though is ease of use of software products, and a proof
assistant is definitely a software product. To get many people to use a
software product, especially one that is not just a minor variation on one
they know, it has to be amazingly simple to use. This of course will be a
huge challenge for this kind of technology.
>
> 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.
>
Ouch. Speaking of ease of use! Actually I had forgotten that this
particular example needs one hint to get the user started: Click with the
mouse on an expression in the problem statement. That will cause a little
menu to appear. This is a very simple problem, but Khan Academy currently
has no way for students to solve practice problems online. They basically
just give an answer. If students solve problems with an online tool, the
Khan Academy system can track every step, not just the final answer. They
analyze student skill development through behavior, so detailed tracking
should be important to them.
And yes, I do think MathXpert points the way in key aspects of usability.
The free trial version should be quite adequate for looking into this.
>
> 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.
>
For those who have read this far, I'd very much like to learn what options
there may be for using ML (or I presume OCaml) for building Web
applications. I'm more than happy to discuss the question, but this proof
assistant is going to need to become a Web application, for a number of
reasons.
Going on to your further points, yes I totally agree that getting serious
adoption requires a lot more than just programming of a core engine. In
fact it will require considerable work figuring out how to hide 99.9% of
the complexity from 99% of the users (numbers approximate). ;-)
>
> 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.
>
Cool, yes. Looking at proofs of recognizable theorems sounds good, though
some of you math heads are probably more suited to that investigation than
I am.
Your various comments about requirements sound good to me, including the
issue of limiting jumps in reasoning. Beeson's retrospective paper "Design
Principles of MathPert" (
http://www.michaelbeeson.com/research/papers/hisc.pdf) I think is well
worth a read. It addresses this and various other issues in educational
math software. He focuses on assisting solution of math problems, but it
his system does rigorous proofs under the hood and the paper seems
perfectly relevant to assisting with proofs of theorems.
>
> 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
I'll take a look there, thanks.
Best regards,
Cris
>
>
> 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
