ProofWiki talk:Current events/ITP 2011

notes

I haven't had usable internet access for a while, but thought I'd try and tolerate the keyboard on my phone to write this:

- I started compiling an english-french maths dictionary for my own benefit (studying in france for a few years), ill post it up when its more complete if its of interest

- The rigidity of proof structure discussion is interesting. I though I should add something along this line: mathematics consists of ideas, the rigor is just a language used to express them. For the site to be an (independent) learning resource both aspects are needed. Maybe a hand wavey discussion of what the theorem really means section? I think line by line deductions alone arent enough. --Linus44 14:39, 4 September 2011 (CDT)

Have to respond here since my phone wont save enough lines. I was thinking about results like a homomorphism of fields is injective, where the implication that the structure theory of fields differs in character from that, say, of rings since up to isomorphism the only relation between fields is "is a subfield of" perhaps isn't clear. So it is potentially possible to understand and even use the result without understanding what it really says.

But then perhaps it's wrong to consider proofwiki an independent learning resource; I rarely learn about a subject from a single textbook, instead I cross reference between two or even more.

This said i cant think of a good, or even practical way of regulating such a notion as I suggested before, a major problem being that no-one will be able to agree "what the result actually means". Perhaps it's best as it is: the proofs happen here, and those seeking woffle (waffle?) can go to wikipedia.

Shrug ... suppose there's no harm in adding a "what this means" section, as long as it doesn't get too messy (and I'm afraid I can't explain what I mean by "messy"). If you feel you're up to exlplaining "why" (and here's another idea: add a "motivation" section) then feel free.

There are already one or two results which have a few lines of explanation at the bottom of them, but these are not consistent. Maybe it's time to revisit that. --prime mover 13:44, 5 September 2011 (CDT)

I guess the reason I wrote despite not having any useful ideas is that I think it is a mistake to go too far in the pursuit of rigor; theres a danger of forgetting why it was needed in the first place. In particular the mention of theorem provers worried me.

IMO the whole raison d'être for this site is purely for the rigour. And if it's structured well enough and the comments are adequate (e.g. "follows from definition of", and "direct application of etc. theorem" and so on) then it learns itself.--prime mover 13:44, 5 September 2011 (CDT)

re: dictionary: my fingers ache and i hope to have decent internet access soon. will write more then --Linus44 08:51, 5 September 2011 (CDT)

Have a good trip. Just don't get stuck in the road works on the E34/E313 south of Antwerp - you'll be there all night. --prime mover 13:44, 5 September 2011 (CDT)

Possibly, but I'd like to see a practical example. As long as we don't go down the following particular route I have an issue with: when a proof is interrupted half way through with paragraphs of digressionary waffle, probably so as to bulk a proof up into something big enough to be published in a paper.

If a proof is not rigorous it's not a proof. On the other hand I can see that it may be useful to have some explanation as to where the proof is going (if it's complicated and has several stages), but it's too easy to lose the thread of an argument if it's included in the bulk of the proof itself.

Maybe for some proofs (give me an example, can't think of many proofs on this site which need the sort of treatment you describe) we could do something like that. But from my perspective, the only difficulty I tend to have with following proofs through is when the writer of a proof takes for granted a step which is based upon the properties of a definition which is ill-formulated (which is where I'm having all sorts of trouble with the Frobenius's Theorem I've been working on today).

So, as I say, give us some examples and we'll see where it goes.

As for the concept of an "English-French dictionary", I think it might work better to put the various translations of the concepts into the entries themselves (in the same format that I put the one for "Field" in place last week). The plan was that I put a template together once I see how it would work when a few translations are put in. So feel free to start adding some of what you have, and it will be a start. --prime mover 15:23, 4 September 2011 (CDT)

Thought more about the dictionary. It could exist happily side by side with the existing definitions, and provide links into the various concepts. That may be easier to manage than the way I suggested. We might even be able to lift the page structure from wiktionary, or whatever. I'm interested to see what you can put together. --prime mover 01:30, 5 September 2011 (CDT)

Re: "Making the proof structures more rigid"

Hello,

You might be interested in Wiedijk's Mathematical Vernacular which is close enough to a rigid, formal proof language. For an example translating a good old fashioned proof (of the squareroot of 2 being irrational) into the vernacular, check out this blog entry.

It's close enough to English as to not cause too many problems, and (in theory) it could easily be translated into a language understood by automatic proof checkers.

Just thought it might be interesting to pass along...

Best, Pqnelson 21:25, 15 October 2011 (CDT)

Excellent. It goes some considerable way in the right direction. Nijmegen again! They are indeed firmly at the forefront here ... --prime mover 06:20, 16 October 2011 (CDT)