I put it in an email to Jean-Pierre Marquis that a proof is conducted in a conceptual landscape: an analogy is that to describe the way to the station we may say: go right, then left and turn right again at the first traffic light. We do not describe the cracks in the pavement; but we might say: beware of the road works. Constructing (finding?) landscapes was Grothendieck's amazing contribution, as suggested by Bill's comments. I am told that computer assisted proofs have had some success, for example in Boolean algebra (every Robbins algebra is Boolean.): we can see that a computer can find its way through a maze, and analogous things should be useful in mathematics generally. The problem seems to be that the computer needs a way of prescribing the appropriate conceptual landscape, analogously to the way we do mathematics, and there is here a need for programming languages which can manage the construction of the variety of hedges in the appropriate high level maze! (see Bill's comments). Even at a given level, it is easy to give problems which are too hard to do by hand: I gave a course at Bangor in which one of the exercises was to find a polynomial in x,y over the reals which had at least 5 critical points, to classify them, and to produce an illustration of the surface (using Grobner basis methods in Maple). There is also an aesthetic element: what do we mean by a good proof? My own route to groupoids (and then higher groupoids), came about because I was trying to write a book on topology in the 1960s including the fundamental group and got fed up with having to get the fundamental group of the circle by an entirely different method, which really needed a development of its own. Raoul Bott said that Grothendieck was amazing in that he was prepared to work very hard to make things tautological: this was also by playing with concepts and producing remarkable things. (I overheard this at the 1958 ICM in Edinburgh.) But Grothendieck wrote to me saying that "Throughout my whole life as a mathematician, the possibility of making explicit, elegant computations has always come out by itself, as a byproduct of a thorough conceptual understanding of what was going on. " Ronnie On 26/04/2011 14:45, William Messing wrote:
I agree with what Andre wrote concerning proofs. Ronnie, you will certainly recall Grothendieck's letter to you in which he recalled that at the first Seminaire Cartan he was initially quite perplexed as to how the singular chain complex of a topological space, gigantic in size, could possibly lead to concrete computations and applications. As he said, he soon realized that it is not the size that matters, but understanding things properly, that is, in the correct order or manner. In the same letter he recalled that initially he was mystified as to how one would ever be able to make concrete calculations in etale cohomology, until, after, as he1 put it, several days of intense thought, he saw that understanding the cohomology of curves, with perhaps arbitrary constuctible torsion sheaves (torsion prime to the characteristic of the field over which one is working) was the key.
Concerning proofs constructed by people as opposed to computer assisted proofs, many years ago Deligne remarked that while he did not believe in computer assisted proofs, he was not going to look for a counterexample to the proof of the four color theorem.
Best regards,
Bill Messing
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]