What's new? | Help | Directory | Sign in
Google
flyspeck
The Flyspeck Project
Project Home
  
Downloads
  
Wiki
  
Issues
  
Source
    
Search
for
Updated Mar 24, 2008 by TCHales
Labels: Featured
FlyspeckFactSheet  

#This is an introduction to the Flyspeck Project, whose purpose is to give a formal proof of the Kepler Conjecture.

The Flyspeck Project Fact Sheet

Flyspeck Google Group

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.

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

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.

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 may take as many as 20 work-years to complete.

How far along is the project? Here are some recent developments. (Updated October 2005)

Should I get involved

This is an undertaking of that has the potential to develop into one of historical proportions. It is not the sort of project that can be completed by a single individual. Instead it will require the collective efforts of a large and dedicated team over a long period. We are actively recruiting collaborators and team members.

We are looking for mathematicians (from the advanced undergraduate level up) who are computer literate, and who are interested in transforming the way that mathematics is done.

Are you excited about the QED manifesto? Are you interested in applying the manifesto to a problem of great historical significance? Please become involved! We need your help.

How do I get involved?

The first step is to learn the relevant background material:

See the resources listed at the bottom of the page for more information about these topics.

The second step is to become an experienced user. In practical terms, this means being able to create your own proof in the HOL light system.

If you have successfully proved a non-trivial theorem in the HOL light system, then contact Thomas C. Hales http://www.math.pitt.edu/~thales if you wish to participate.

Resources

Objective CAML

Learn to program in Objective CAML

HOL light

The Kepler Conjecture

Books giving Geometry background

The first two books are intended for undergraduates.

Popular Material On Flyspeck


Sign in to add a comment