Dear Andre, In connection with the current discussion on explanatory proofs, and more particularly about the difference between computer generated proofs and human ones, I have something to add to what you wrote --drawn from my own experience. Humans do not have either the speed or the ability to hold the enormous amounts of information that machines do. On the other hand, the only way to see the big picture is speed of reasoning coupled with intuition - naturally without checking the details at each step. That way, two things may happen to humans of which computers are free of: (1) errors are made, and (2) new ideas originate. Errors are not a good thing,  of course, but they are a possible outcome from taking risks, without which no new ideas would ever surface. Working out the details of that first glimpse of the truth may be painful, but necessary.  It may lead to truth (hardly ever), or to further glimpses. I agree with you that the sequence intuition --> computation---> intuition---> computation-->.... is the only available course of action for a good mathematician. With luck, the sequence terminates eventually, and it does in truth. But it must begin with intuition. Some of my collaborators have expressed surprise at my starting any investigation with a title and an abstract, when they would leave both for the end. Naturally, that title and abstract may very well change at the end of the investigation, but if I were incapable to see the big picture at first, I would not begin any work at all. A final trivial thought - computation alone is not mathematics, and neither is intuition alone. The former is typical of machines, whereas the latter is typical of artists.  Best regards,Marta ----------------------------------------

Date: Mon, 25 Apr 2011 22:01:05 -0400 Subject: categories: Re: Explanations From: joyal.andre@uqam.ca To: jds@math.upenn.edu; ronnie.profbrown@btinternet.com; graham@eecs.qmul.ac.uk

Dear Jim,

You are perfectly right! I am always amazed by the fact that a computation can yield a surprising result. It is as if the formal system knew more than me! Actually, I find a computation boring when the result is not surprising. Computing is probably the main vehicule by which we can move beyond a given body of intuitive knowledges. But after the initial surprise, we try hard to integrate the new result in a larger body, where it may become less surprising. It may even become obvious!

The chain

intuition--->computation---->intuition--->computation.....

is probably more important than the chain

proof--->method---->proof--->method.....

André

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]