[FOM] Formalization Thesis

joeshipman@aol.com joeshipman at aol.com
Mon Jan 28 01:09:23 EST 2008

This was discussed a few years ago here. My take is that the 
mathematicians who understand these visual proofs have always been able 
to fill in enough details when pressed, that those who can't "see" 
things the same way will still accept the proof.

However, this is an empirical observation, and I have no a priori 
reason to believe it should always be true; and it may require a great 
deal of work by both prover and verifier, so there ought to be 
borderline cases where it has not yet been done to everyone's 

In other words, something essential is lost in taking out the "visual" 
elements of the proof; but the result of this formalization, though 
unsatisfactory by some criteria, still preserves enough meaning that 
the theorem in question is not doubted.  (It would be remarkably 
interesting to have a counterexample, which would represent a type of 
impasse that, while not unprecedented in the history of mathematics, 
has not been seen for many decades.)

Another way in which mathematics may fail to be fully formalizable 
today involves the work of mathematical physicists like Witten, who 
often use physical intuition and principles of theoretical physics to 
argue that certain results in pure mathematics ought to be true -- 
their track record has been quite good, good enough to get Witten a 
Fields Medal, and I'm not sure that the failure to reduce much of this 
work to ZFC-theorems justifies dismissing it as "not mathematics".

-- JS

-----Original Message-----
From: Timothy Y. Chow <tchow at alum.mit.edu>
To: fom at cs.nyu.edu
Sent: Sat, 26 Jan 2008 3:08 pm
Subject: Re: [FOM] Formalization Thesis

Arnon Avron wrote:
>However, it is very doubtful that all geometric concepts and methods 
>proofs can be faithfully expressed in discrete languages.

I can see the intuition behind your doubts, and there is some force to
them.  Suppose we grant your hypothesis for a moment.  What then is 
attitude towards geometric proofs of geometric results that not 
seems to be able to "see"?  Jaffe and Quinn touched on this subject in
their famous article on "Theoretical Mathematics":


An important part of the culture of mathematics is that a proof should, 
principle, be checkable by anyone who is willing to put in the effort.
The fact that certain proofs, such as that of the four-color theorem or 
the classification of finite simple groups, threaten to violate this
principle is what lies behind the complaints that one sometimes hears
voiced about them.

The notion that some geometric proofs may be *fundamentally*
"undiscretizable" threatens to violate the same principle in a 
way.  My current instinct is to say that when Thurston gives a 
proof of a geometric result which others can't quite follow, it's 
he has left out details, and if he gave those details then anyone else
could check the proof.  But there's an alternative view, which is that
there *aren't* any missing details; some proofs may be visualizable by
some people but not by others, and there may not be *any way at all* 
the visually impaired to check the proof.  Would you be willing to go 
far as this, when you argue that geometry defies discretization?

Something similar happens in set theory; if someone claims to be able 
visualize inaccessible cardinals then he can "prove" that ZFC is
consistent, and someone who lacks that ability cannot check the proof.
But in the set-theoretical case, the statements in question can be
discretized, and the offending "unvisualizable" statements can be 
formulated as specific, discrete *axioms*.  The conceptually impaired 
verify everything except the *truth* of said axioms, and hence the
"damage" is contained and limited.

But if methods of geometrical proof cannot be discretized, then I don't
see how the damage can be limited in such a clean manner.

FOM mailing list
FOM at cs.nyu.edu

More new features than ever.  Check out the new AOL Mail ! - 

More information about the FOM mailing list