[FOM] Formalization of visual proofs (was Re: Shapiro)

[Mitchell Harris]

On Tue, 30 Nov 2004, Timothy Y. Chow wrote:

>Joe Shipman clarified what he was asking for; to test my understanding, 
>let me suggest two candidates:
>
>1. Every finite graph can be embedded in R^3 without crossings.
>
>2. The trefoil knot cannot be unknotted in R^3.
>
>Both of these are visually obvious, and it seems any kind of formalization 
>is likely to lose something in the translation.  Do these then qualify?
>
>Vladimir Sazonov questions whether any so-called visual proof is really 
>anything more than a heuristic starting point if it's not clear how to
>formalize it.  What do you say about #2 above?  This strikes me as an
>example of something that is as obviously true as any standard axiom,
>yet which I wouldn't call "linguistic" (even if one admits visual 
>languages).  It's also not immediately clear how to formalize it, but
>formalization seems to reduce the clarity and certainty rather than to
>increase it.

What is the point of formalization? If it is getting in the way of 
understanding a particular proof, it's getting in the way as 
annoying details that are probably meant only ostensibly or for a 
machine (that is, such details are only taxing our capacities as humans). 
If the formalization is reducing the certainty, then the 
idea isn't so certain to begin with or it's a bad formalization.

This holds whether the formalization is symbolic or visual/kinesthetic or 
ad hoc.

-- 
Mitch Harris
Lehrstuhl fuer Automatentheorie, Fakultaet Informatik
Technische Universitaet Dresden, Deutschland
http://lat.inf.tu-dresden.de/~harris