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

[Josef Urban]

I don't see a good reason why the machines would not eventually

- generate a human-level proof linked to the formal one (whatever the
methods for proof finding); this should include pointing out the ideas
interesting on the human level

- verify a high-level proof idea, and if an unusually big gap is
filled while doing that or if the gap is filled in a surprising way,
report it to the human author

- try to translate back from algebraic proofs to "intuitive" proofs of
all kinds if there is good link

We already have some basic methods for some of these things - like
estimating the value/interestingness of lemmas, but it's really just
the beginnings.

Josef


On Wed, Dec 30, 2015 at 3:38 AM, Timothy Y. Chow <tchow at alum.mit.edu> wrote:
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom