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

[Timothy Y. Chow]

A piece of old news that I only recently became aware of was that about 
halfway through the Flyspeck project (i.e., about five years ago), they 
discovered that there was a non-trivial gap in the original version of the 
proof.  Details here:

http://www.cl.cam.ac.uk/~jrh13/papers/revkepler.pdf

I'm guessing that many FOM readers were not aware of this either, because 
nobody mentioned it back in October 2014, when Hendrik Boom and Adriano 
Palma asked a related question.

http://www.cs.nyu.edu/pipermail/fom/2014-October/018206.html

To quote Palma: "Are there cases in which the check in terms of syntax 
done by the machines revealed a real flaw in a proof, in the informal or 
intuitive style?"  Admittedly, the gap above did not cause anyone to doubt 
the truth of the Kepler conjecture, and it was fixed pretty quickly, but 
it was a real gap, and would probably not have been discovered if Hales et 
al. had not pursued the Flyspeck project.

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.

However, the aforementioned gap in the proof of Kepler got me thinking. 
In some sense, the proof wasn't *wrong*.  It was just assumed that a 
certain step was straightforward---"without loss of generality we may 
assume..."  The step was in fact correct, but there was a subtlety that 
had been overlooked.  We can even bill this as a success story, because it 
demonstrates that the process of formalization can not only detect gaps 
but it can draw our attention to subtleties and thereby increase our 
understanding.

But suppose that the proof assistant had been a lot more "intelligent" 
than today's proof assistants are, and had *figured out on its own how to 
plug the gap*.  Then we humans might never have become aware that there 
was a subtle point that had been overlooked.  The critics would then have 
been at least partially vindicated: The machinery of formal proofs would 
have stolen away an opportunity for deeper understanding.

Admittedly, in this case, even if a proof assistant had plugged the gap, 
the "lost insight" would not have been a big loss to mathematics.  After 
all, the argument amounted to showing that a certain weird situation was 
not a real possibility, so who really cares?  As proof assistants become 
more intelligent, however, perhaps their ability to fill gaps in reasoning 
could "hide" bigger and bigger insights.

In one sense, this issue is not new.  There is already a danger that we 
could become over-reliant on Groebner basis algorithms and miss geometric 
insights, or over-reliant on WZ-style identity provers and miss 
combinatorial insights.  Atiyah is reported to have said: "Algebra is the 
offer made by the devil to the mathematician.  The devil says: `I will 
give you this powerful machine; it will answer any question you like. 
All you need to do is give me your soul: give up geometry and you will 
have this marvellous machine.'"  Still, proof assistants potentially take 
this Faustian bargain up to a new level.  I, for one, would still welcome 
our new theorem-proving overlords, but with more sympathy for the critics 
that I previously dismissed.

Tim