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é -------- Message d'origine-------- De: jim stasheff [mailto:jds@math.upenn.edu] Date: lun. 25/04/2011 20:52 À: Joyal, André Cc: Ronnie Brown; Graham White; categories@mta.ca Objet : Re: categories: Re: Explanations On 4/25/11 9:51 AM, Joyal, André wrote:
The goal of a human proof is to convince other peoples of the truthfulness of a proposition. It is by nature explanatory and it can lead to new insights. I disagree mildly.
convincing other people of the truthfulness of a proposition can involve staightforward computation which I don't find explanatory jim [For admin and other information see: http://www.mta.ca/~cat-dist/ ]