Flyspeck Project Fact Sheet

The Flyspeck Project Fact Sheet

Flyspeck Project Home

Introduction

The purpose of the flyspeck project is to produce a formal proof of the Kepler Conjecture. This page gives some basic facts about this project.

What does the name mean?

The name flyspeck comes from matching the pattern /f.*p.*k/ against an English dictionary. FPK in turn is an acronym for "The Formal Proof of Kepler." The term flyspeck can mean to examine closely or in minute detail; or to scrutinize The term is thus quite appropriate for a project intended to scrutinize the minute details of a mathematical proof. More expansively, FLYSPECK is the Formidably Long, Yet Systematic Proof by Exhaustion of the Conjecture of Kepler (as suggested by G. Lawlor).

What is a formal proof?

A formal proof is understood in the sense of the QED manifesto

To learn more about formal proofs, see Freek Wiedijk's web pages Also see the complete works of John Harrison.

How does a formal proof differ from a traditional mathematical proof?

Traditional mathematical proofs are written in a way to make them easily understood by mathematicians. Routine logical steps are omitted. An enormous amount of context is assumed on the part of the reader. Proofs, especially in topology and geometry, rely on intuitive arguments in situations where a trained mathematician would be capable of translating those intuitive arguments into a more rigorous argument.

In a formal proof, all the intermediate logical steps are supplied. No appeal is made to intuition, even if the translation from intuition to logic is routine. Thus, a formal proof is less intuitive, and yet less susceptible to logical errors.

What are the specific tools that will be used in the flyspeck project?

All the formal proofs will be made by computer and programmed in the Objective CAML programming language.

The steps of the proof will be generated by computer programs using John Harrison's HOL light software package, with contributions from other systems such as Coq and Isabelle, as described below.

The design of the proof will be based on the 1998 (traditional-style) proof of the Kepler Conjecture by Hales and Ferguson.

What is the Kepler Conjecture?

The Kepler Conjecture asserts that the density of a packing of congruent spheres in three dimensions is never greater than pi/sqrt(18), or approximately 0.74048. This is the oldest problem in discrete geometry and is an important part of Hilbert's 18th problem. An example of a packing achieving this density is the face-centered cubic packing.

The problem remained unsolved for nearly 400 years until it was finally cracked in 1998.

Why give a formal proof of the Kepler Conjecture?

The proof of the Kepler Conjectures is one of the most complicated mathematical proofs that has ever been produced.

The Annals of Mathematics solicited the paper for publication in 1998 and hosted a conference in January 1999 that was devoted to understanding the proof. A panel of 12 referees was assigned to the task of verifying the correctness of the proof.

After four full years, Gabor Fejes Toth, the chief referee, returned a report stating that he was 99% certain of the correctness of the proof, but that the team had been unable to completely certify the proof.

Robert MacPherson, editor of the Annals, wrote a report that states

The news from the referees is bad, from my perspective. They have not been able to certify the correctness of the proof, and will not be able to certify it in the future, because they have run out of energy to devote to the problem. This is not what I had hoped for.

He continues with comments to Hales that may well mark a profound change in the way that mathematics is done:

The referees put a level of energy into this that is, in my experience, unprecedented.
They ran a seminar on it for a long time. A number of people were involved, and they worked hard. They checked many local statements in the proof, and each time they found that what you claimed was in fact correct. Some of these local checks were highly non-obvious at first, and required weeks to see that they worked out. The fact that some of these worked out is the basis for the 99% statement of Fejes Toth that you cite. One can speculate whether their process would have converged to a definite answer had they had a more clear manuscript from the beginning, but this doesn't matter now.

Fejes Toth thinks that this situation will occur more and more often in mathematics. He says it is similar to the situation in experimental science - other scientists acting as referees can't certify the correctness of an experiment, they can only subject the paper to consistency checks. He thinks that the mathematical community will have to get used to this state of affairs.

You may ask whether this degree of certification is enough checking for a mathematical paper, and whether it's not in fact comparable to the level of checking for most mathematical papers. Both the referees and the Editors think that it's not enough for complete certification as correct, for two reasons. First, rigor and certainty was what this particular problem was about in the first place. Second, there are not so many general principles and theoretical consistencies as there were, say, in the proof of Fermat, so as to make you convinced that even if there is a small error, it won't affect the basic structure of the proof.

The Annals is confident enough in the correctness that they will publish a paper on the proof. However, this paper has brought about a change in the journal's policy on computer proof. It will no longer attempt to check the correctness of computer code.

There is a way to proceed that more fully preserves the integrity of mathematics. This is the way of formal proof.

What is Objective CAML?

CAML light is a functional programming language in the ML family. Tutorials on CAML can be found at the bottom of this page. The Objective CAML language was selected for this project because HOL light is written in this language.

What is HOL light?

HOL light is a computer program that produces carefully checked mathematical theorems. HOL light is John Harrison's reimplementation of HOL in the Objective CAML language. HOL light was selected for the project because

• The system is built on a small kernel, and the type checking insures that no fatal bugs can occur outside the kernel. That is, if you leave a bug in your code, the worst that can happen is that you will fail to prove a theorem you hoped to prove. You can never put a bug in your code that yields a false statement.
• The system becomes self-checking after the first thousand lines of code.
• The source code is short and quite readable. Thus, any questions about the behavior of the system can be resolved through the syntax and semantics of the underlying language (Objective CAML).
• Objective CAML is a pleasant language to work with.
• The code is highly portable.
• The system is readily extensible.
• The system performed well under informal tests.
• Legend has it that Harrison produced his proof in HOL light of the fundamental theorem of algebra in a single weekend.

In the system there is a "theorem" data type. Each value of this type is the statement of a mathematical theorem. The type checking system in Objective CAML prevents the creation of a value of this type, except by rules that insure that the statement has a proof.

Thus, for instance, if someone succeeds in creating a theorem value in HOL light expressing the statement 'The Riemann hypothesis is true,' then the world can be confident that the Riemann hypothesis is true.

Using the HOL light code, functions can be written in Objective CAML whose output are values of type theorem. For instance, it is possible to write a function approx_pi whose input is an integer n and whose output has type theorem |- abs(pi- x) < 10^-n`, where x is a rational number. That is, it produces a proof that a given rational approximation to pi is valid. (Such a function has been written by Harrison.)

How does HOL light differ from packages such as Mathematica?

In Mathematica, it is also possible to write a procedure whose input is n and whose output is a rational number x such that abs(pi-x) < 10^-n. However, the Mathematica procedure

ApproxPi[n_]:=Rationalize[N[Pi,n+1],10^-n]

relies on algorithms that are unknown origin and unknown reliability. What does N[Pi,n+1] do behind the scenes? How reliable is it? Can you prove this line of code always does what you wanted? Or do you detect a subtle bug?

In HOL light, by the time it returns a value of type theorem |- abs(pi-x) < 10^-n the computer has checked every logical step in the derivation. Thus, results obtained form HOL light are much more reliable than those in Mathematica.

What is the goal of the flyspeck project?

The purpose of the flyspeck project is to produce a value of type theorem in HOL light that expresses the statement 'The Kepler Conjecture is true.'

How large a project is the flyspeck project?

The project has about 500,000 lines of code.

Resources

Objective CAML

Learn to program in Objective CAML

• The official CAML website
• Introduction to the Objective Caml Programming Language by Jason Hickey (pdf book)
• Developing Applications with Objective Caml (O'Reilly book)

HOL light

• The official HOL-Light site
• Manual (PDF)

The Kepler Conjecture

• "Cannonballs and Honeycombs" An introduction for a general mathematical audience to the ideas of the proof of the Kepler Conjecture.
• The tex files for the most recent version of the proof can be found under the source tab of this project.
• A historical overview of the Kepler Conjecture, tracing the problem to a pamphlet published by Kepler in 1611.
• The mathematical text of the proof.

Books giving Geometry background

The first two books are intended for undergraduates.

• Euclidean and non-euclidean geometry: an analytic approach, by Patrick Ryan. This is an undergraduate level textbook that gives useful background in spherical trigonometry
• Euclidean Geometry and Convexity, by Russell Benson. An undergraduate level treatment length, plane area, surface area, volume, and convex bodies.
• Algorithmic Geometry, by J-D Boissonat and M. Yvinec. This book gives algorithms for finding convex hulls, linear programming, triangulations, Voronoi diagrams, Delaunay triangulations
• Computational Geometry: algorithms and applications, by M. de Berg et al. This book covers convex hulls, line segment intersections, polygon triangulations, linear programming, Voronoi diagrams, Delauany triangulations, binary space partitions.
• Lagerungen in der Ebene, auf der Kugel, und im Raum, by L. Fejes Toth Ignore the other recommendations, and study this book before all others.