FOM: mathematical certainty

[Stephen Cook]

I feel I should reply to Randy Pollack's last message, since he is speculating
about what FOM readers think.   He says
	 
	 Further, I suppose many FOM readers feel Fermat's Last Theorem is
	 mathematically certain, while the four-color theorem is not, although
	 most of us have not directly checked either proof.  

My point of view is that "mathematically certain" means that there exists a formal
proof in an appropriate formal system; say ZFC.  The authors of both theorems
are trying to convince us that such a proof exists.   I don't know which (group
of) author(s) has done the more convincing job, but the necessary use of computers
to check the four-color theorem proof does NOT make it less convincing.   Both
computers and mathematicians can make mistakes:  to decide which argument is more
convincing one has to consider who checked each one and how it was checked.
In the case of the 4CT, part of the checking should involve writing an inpendent
computer program and running it on a different computer.

Steve Cook