My suggestion is that mathematical proofs still require a mathematical landscape in which to find our way. Michael Barr points out the problems of finding a completely `logical' proof. I propose the analogy of giving directions to the station, such as `go out of the house, turn right, go straight on until ..., etc., etc.' We don't need to specify all the cracks in the pavement, but we may need to warn of holes due to roadworks! The aura of certainty in a mathematical proof is partly because the `conceptual landscape' has been worked up over centuries, in terms of convenience and usability, and tested by thousands. Hopefully, arguments come to be produced which seem inevitable, indeed aesthetic, rather than ad hoc. Are there computer theorem provers which can work at a `landscape level'? The assumption is also that there are no cracks in our mathematical universe. On the more general point, I did hear of a University Vice Chancellor who asked his staff for a series of lectures on `The notion of validity in my subject'. Ronnie Brown [For admin and other information see: http://www.mta.ca/~cat-dist/ ]