[FOM] Gap in the original Hales-Ferguson proof of Kepler

[Walt Read]

On Tue, Dec 29, 2015 at 6:38 PM, Timothy Y. Chow <tchow at alum.mit.edu> wrote:
>
> This incident also prompted me to consider something that had not occurred
> to me before.  To explain, let me first back up a step.  Critics of formal
> proofs sometimes complain that formal proofs promote the wrong attitude
> towards mathematics; proof should be about *understanding*, they argue, and
> an unintelligible proof that has been mechanically verified has very little
> value.  This criticism has always struck me as misguided, because there is
> nothing to stop us from generating a humanly understandable proof in
> addition to the formal proof.  Indeed, by eliminating any worries we might
> have about correctness, it frees us to spend more time on understanding, as
> opposed to tedious verification.
>

It seems to me that this point of view leads to a form of the "moral
hazard" problem that, notably, economists discuss. I have often heard
informal, "intuitive" explanations of mathematical results that were
presumably intended to enhance understanding, in some sense of the
word, but which were more misleading than helpful. (Look at many
popularizations of Goedel incompleteness, for example.) Because we're
sure the result is correct, we can wave off any resulting confusion
with, at most, "I guess I should have been clearer", rather than
reconsidering the possibility that we should instead fundamentally
rethink our explanation. If the result hasn't been verified - formally
or informally - then the possibility that it's actually wrong, at
least as stated, provides a reality check on any claims of achieving
understanding. Personally, I find the possibility of being wrong is a
great incentive to put in the effort to go beyond the mechanics and be
sure I really do "understand" the result.

-Walt