7 views

Skip to first unread message

Nov 22, 2008, 3:03:52 AM11/22/08

to vdash

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.

Nov 22, 2008, 10:09:25 AM11/22/08

to vd...@googlegroups.com

Hello. Below are some comments on the previous ideas, and I've put my

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.

>

How would one authenticate their education level? If the wiki's

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.

That's how I got here.

I think using LaTeX formatting is a great idea, as most of us in the

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.

>

Ironically, being conversant in formal proofs is assumed!

>

> 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 :)

>

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.

>

> 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.

I agree that vdash is an important project. It both helps the general

user and expands the field for mathematicians. Thanks to Cameron for

getting this started and having accessibility in mind.

>

> >

>

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.

>

> >

>

Nov 22, 2008, 12:04:34 PM11/22/08

to vd...@googlegroups.com

> 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)

Nov 22, 2008, 3:56:42 PM11/22/08

to vd...@googlegroups.com, avi...@cmu.edu

Hi!

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

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

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu