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

[Lawrence Paulson]

> On 30 Dec 2015, at 02:38, 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

In the field of machine-assisted proof, it is well known that formalising almost any mathematical material will throw up small gaps. Mostly they are simply "obvious" steps; more rarely, overlooked degenerate cases.

My favourite instance of a gap is in the thesis of my former PhD student, Jacques Fleuriot, who found a way to formalise the infinitesimal proofs in Newton's Principia using a combination of geometry and non-standard analysis.  While formalising one of Newton's proofs, he identified a step in which the infinitesimal reasoning was not valid according to NSA. Fortunately, there was another way to reach the desired conclusion. See steps (25)-(27):
http://www.cl.cam.ac.uk/~lp15/papers/Isabelle/fleuriot-kepler.pdf

There is no tension between the wish for formalised proofs and the wish for intelligible proofs. Obviously, formal proof languages are not very intelligible at the moment, but they are getting better. With the exception of Euclidean geometry, which is decidable, very few statements worthy of being called theorems can be proved automatically using any technology. Two counterexamples are Cantor's theorem (which is very easy to prove anyway) and the Robbins conjecture. The latter was proved by McCune using a specialised tool, and the calculation was later expressed as an intelligible proof.

Larry Paulson