[FOM] Re: Shapiro on natural and formal languages

[Timothy Y. Chow]

Joe Shipman wrote:
> I believe Avron, in speaking of "geometrical ways of reasoning", was 
> referring not (as Sazonov seems to suppose) to classical Euclid-style 
> proofs , which can be put into a formal language relatively 
> straightforwardly, but to what I prefer to call "visual proofs", where 
> it is possible in practice for a mathematician to follow the proof only 
> if he "has a picture in his head".

In a couple of your older articles that you linked to, you asked for 
examples of visual proofs that are not obviously translatable into a 
formal language.  I didn't see any examples presented.

Jaffe and Quinn's famous article on "theoretical mathematics" might 
provide more specific pointers on where to look:

   http://www.ams.org/bull/pre-1996-data/199329-1/jaffe.pdf

However, as I thought more about your question, I realized that it's much 
more slippery than I thought at first.  Let me put it this way: Why do you 
think that low-dimensional topology is a good place to look?  Presumably 
it's because highly abbreviated "proofs by pictures" show up a lot there. 
But mathematicians (in any field) never publish proofs that have every 
single step filled in.  Visual proofs are no exception, and when (say) a 
geometer gives a complex pictorial proof, it is understood that there are 
details that need to be filled in, but that it is easy to do so.

So I think what you are looking for is *not* a highly technical proof
that the experts consider "obvious" yet where the actual process of 
formalization is very involved, because the *reason* the experts consider 
such visual proofs "obvious" is *not* that they are "irreducibly" obvious 
(which is what I think you really want) but that because of their 
experience it is obvious how to flesh out more detail upon request.

Geometry might still be a good place to look, but one needs to search for 
arguments that are "obvious" because they *can't* be fleshed out further, 
not arguments that are "obvious" because experienced geometers can see at 
once how to fill in the details.

Furthermore, there's another pitfall, which is that if some point *can't* 
be fleshed out further, there's always the possibility that it's because
the proof actually has a gap.  In fact this is what often happens: Some
visual proof is accepted as correct for a while, and then people start 
trying to flesh it out and run into something that they can't prove.
The usual reaction is to identify this as a gap in the proof.  Perhaps
if the same "gap" kept showing up often enough then it might be given 
the status of a new and intrinsically visual axiom, but even non-experts
would probably hear about this kind of news pretty quickly.

Tim