FOM: Final reply to Hayes on proofs

[Joe Shipman]

Hayes:
>No, that is exactly what I mean. A proof, strictly speaking, should be
>completely formalised and mechanically checkable. I believe this is
>essentially the accepted standard of a completely rigorous proof throughout
>most of mathematics, in fact. While many published proofs, being intended
>for reading by human beings, dont meet that impractical standard, if there
>is any point of doubt or debate in a proof, it is expected that the authors
>of it could, in principle, provide all the relevant details. It will never
>be acceptable in mathematics to just say that some conclusion is 'obvious',
>if challenged to account for the reason for it.I am glad to see that you are
consistent in not drawing a line short of a fullyformalized proof.  But it is not
really fair to critique my "proofs" for fallingshort of this standard, because all
published proofs do -- the reason we evenbother to come up with formal systems is
because we can convince ourselves that thetedious details COULD eventually be filled in
for the types of proofs we generallyconsider valid.  There is no basis to distinguish
my "visual" proofs from anyother proof that mathematicians actually communicate to each
other IF it is clearthat the argument is formalizable, and the whole reason for my
introducing theseexamples is that the process by which one would formalize these proofs
is soartificial and contrary to the spirit of the proofs that, although a specialist
canindeed easily see that formalization is achievable, the "infrastructure" requiredfor
this is of a level of sophistication far beyond what is required to
*genuinely*understand the proof as given.  I am hoping that these examples can help
uselucidate some "principles of visual reasoning" that could be rigorously provedonce
and for all, and then applied to rigorize my arguments in a smoother and morenatural
way.

-- JS