Some suggestions...
virtual
The main point of this post is a suggestion: Make the wiki accessible
to anyone with a bachelor's degree level knowledge of math, not
necessarily in logic. There really is a niche for a website to make
formal proofs accessible to the mathematical masses.
A lengthy rant follows:
vdash has been mentioned once or twice on Slashdot.
This is cool because I've been interested in formal mathematics for a
while now.
But it seems to be really tough for a beginner to break into this
area...
It seems that Isabelle/ISAR is something I want to download and start
learning. I haven't figured out what the relationships are between
Isabelle, HOL, ZF, ISAR, etc. are.
The Isabelle reference manual at http://isabelle.in.tum.de/dist/Isabelle/doc/isar-ref.pdf
isn't much help. It doesn't really give you a good sense of the
pieces you need to install, nor does it have much useful description
of the Isabelle language. Its description starts out with a 20-line
BNF grammar and just gets more obtuse from there. The "tutorial" at
http://isabelle.in.tum.de/dist/Isabelle/doc/isar-overview.pdf isn't
much better. The lecture notes at http://www.cs.colorado.edu/~siek/7000/spring07/isabelle-notes.pdf
are a marginal improvement, and might be of minimal use if I actually
get Isabelle up and running, although those notes don't explain such
unimportant details as what the entire file should look like, i.e.
required header and footer boilerplate, how to install and invoke
Isabelle/ISAR, or how to type all the funny math symbols -- it seems
that it must be generated from some TeX or LaTeX markup, but without
knowing specifics that isn't much help. Also, do I *really* need to
use Proof General? For a guy like me who grew up using Windows-world
editors, Emacs is extremely intimidating; I can barely use vi and for
any non-trivial editing I really want to use a text editor with all
the "standard" keys and settings for marking and cursor movement.
Anyway, I've been working with and programming computers almost my
whole life, I'm a reasonably adept Linux user, I have a bachelor's
degree in mathematics (my specialization was in abstract algebra, but
I did take a course in math logic covering semantic vs syntactic
application, computability, propositional logic, FOL, Godel's
incompleteness theorem, etc.)...but I've found the world of formal
mathematical proof to be rather inaccessible. Many of the documents
that exist seem to assume you're very familiar with formal proof
systems already and just need to know the details of a particular
system.
I would volunteer to help, but my life is kinda busy right now, and it
seems like I don't know enough to really contribute anything
worthwhile. I'll definitely look forward to the day I can contribute
proofs to vdash :)
Anyway, I just wanted to bring it to your attention that there are
serious barriers to entry for people like myself to interact with
formal mathematics, and I think one of the goals of vdash should be to
bring formal mathematics to a wider audience.
Ben Payne
responses to the previous email below their motivating quotes.
My question for Cameron is whether a non-mathematical framework could
be built in the meantime. For example, will the wiki have both the
formal proofs and readable comments along side the math? If yes, could
we start working on the explanation parts? Then when vdash is ready,
the math would just need to be filled in. It seems there is an eager
audience to help, so establishing a framework would let the community
start work. I'm not sure if this is possible, or if it appropriate.
In addition, hosting and managing a wiki is a job in and of itself,
and may distract from the primary goal of getting the math side of
vdash to work. On the other hand, it may give insight as to the
direction and needs of vdash.
On Sat, Nov 22, 2008 at 2:03 AM, virtual <fina...@gmail.com> wrote:
>
>
> The main point of this post is a suggestion: Make the wiki accessible
> to anyone with a bachelor's degree level knowledge of math, not
> necessarily in logic. There really is a niche for a website to make
> formal proofs accessible to the mathematical masses.
>
purpose is to be "accessible to the mathematical masses," how does
education level matter? A proof is a proof, regardless of who typed
it in. First, there is the protection provided by the wiki framework
that shouldn't allow invalid mathematical statements to be made.
Second, most users won't understand the fine details. There will be a
self-selection of who adds to the wiki, based on whether a user can
understand what's going on.
>
> A lengthy rant follows:
>
> vdash has been mentioned once or twice on Slashdot.
sciences know how to write in it, and there are many front ends that
are meant for LaTeX, such as TexNicCenter and Scientific workplace.
If vdash can build on existing infrastructure, it will mean a lower
learning curve. Same sentiments for using a wiki interface.
>
> Anyway, I've been working with and programming computers almost my
> whole life, I'm a reasonably adept Linux user, I have a bachelor's
> degree in mathematics (my specialization was in abstract algebra, but
> I did take a course in math logic covering semantic vs syntactic
> application, computability, propositional logic, FOL, Godel's
> incompleteness theorem, etc.)...but I've found the world of formal
> mathematical proof to be rather inaccessible. Many of the documents
> that exist seem to assume you're very familiar with formal proof
> systems already and just need to know the details of a particular
> system.
>
>
> I would volunteer to help, but my life is kinda busy right now, and it
> seems like I don't know enough to really contribute anything
> worthwhile. I'll definitely look forward to the day I can contribute
> proofs to vdash :)
>
filled in comparatively quickly, leaving little work for the rest of
us non-mathematicians.
>
> Anyway, I just wanted to bring it to your attention that there are
> serious barriers to entry for people like myself to interact with
> formal mathematics, and I think one of the goals of vdash should be to
> bring formal mathematics to a wider audience.
user and expands the field for mathematicians. Thanks to Cameron for
getting this started and having accessibility in mind.
>
> >
>
Slawomir Kolodynski
> A proof is a proof, regardless of
> who typed
> it in.
Yes, that's the beauty of formalized mathematics. I can be a chimpanzee and it will not matter, as long as the proofs I write are correct. This barrier is high enough that no other credentials are needed.
> My guess is that once the system works, the
> "easy" proofs will be
> filled in comparatively quickly, leaving little work for
> the rest of
> us non-mathematicians.
I disagree. There will be plenty of easy proofs to do for years. In fact this is one of the obstacles of formalized mathematics. You don't get credit in academia for formalizing the easy stuff. But you have to have it done before formalizing more advanced material. So a typical mathematician faced with the prospect of spending years of work before even getting to the part which interests her just gives up and says that the library is not extensive enough for serious research. The people who can overcome this problem are those who don't have to show publishable results in their resumes to earn their living. Like me - I am a software engineer.
> It seems there is an eager
> audience to help, so establishing a framework would let the community
> start work.
If you are willing to bet your effort on the assumption that Vdash will be based on Isabelle/ZF and IsarMathLib, then you can install Isabelle with ZF logic (download http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/ZF_x86-linux.tar.gz rather than HOL_x86-linux.tar.gz), download [IsarMathLib sources](http://download.savannah.gnu.org/releases/isarmathlib/http://download.savannah.gnu.org/releases/isarmathlib/isarmathlib-1.6.5.tar.gz) and start learning Isar (note I am biased in this advice as IsarMathLib is my project).
While doing this do share the difficulties and questions on this list (or [IsarMathLib list](http://lists.nongnu.org/mailman/listinfo/isarmathlib-devel) ). This will build the community knowledge and gather material for a tutorial on crafting formal proofs in Isar and Isabelle/ZF. To my knowledge there is no such tutorial yet.
> > But it seems to be really tough for a beginner to
> break into this
> > area...
This is true, I know from experience. But it does not have to be that way.
> Also, do
> I *really* need to
> > use Proof General?
For formal proofs, I am afraid the practical answer is yes. The reason for that is that the front end interacts with Isabelle and only ProofGeneral can do that now. It is not that bad, it can be Xemacs actually, not Emacs, it is nothing like vi. I often use a more modern editor for writing the informal parts, which are more than half of the volume of [IsarMathLib proof document](http://www.nongnu.org/isarmathlib/IsarMathLib/document.pdf).
Slawekk
http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)
Matthew Wampler-Doty
I'm a MSc of Logic student there at the ILLC in Amsterdam. I'm also
here because of slashdot, and because I'm hoping to work on Flyspeck
next summer.
I figured I'd weigh in with a couple of points:
(1) The best way to get started in Isabelle, IMHO, is to attend the CMU
Summer School in Logic and Formal Epistemology. This program is run by
Jeremy Avigad, who formalized the prime number theorem in Isabelle. The
program is open to most students (from bachelors to PhD), and the most
important prerequisites are a strong background in logic and in. I have
CCed Jeremy to this email; he may have notes he is willing to share for
students and ideas for this project.
(2) Is ZF the only logic framework which vdash will support? I ask
because I know there is a lot of existing work that has already been
done with HOL. In all likelihood, a port from HOL to ZF for any theory
is probably not so bad (maybe automatable?), but I'm still a little
curious what the exact motivation for this move is. My apologies if the
motivation for this was already given in a previous post.
And of course, I have lots of ideas for features and design philosophy,
but I'm sure Cameron is inundated already with opinions.
~Matt