August 10, 2014We are pleased to announce the completion of the Flyspeck project, which has constructed a formal proof of the Kepler conjecture. The Kepler conjecture asserts that no packing of congruent balls in Euclidean 3-space has density greater than the face-centered cubic packing. It is the oldest problem in discrete geometry. The proof of the Kepler conjecture was first obtained by Ferguson and Hales in 1998. The proof relies on about 300 pages of text and on a large number of computer calculations. [...]
I wonder if their proof process generated a certificate that would allow a single computer to verify their result in a reasonable amount of time?
Depends on what you define as reasonable time. From what they tell, this does not seem out of reach for the interested layman. 5000 processor hours, most of it perfectly parallelizable on a typical modern desktop takes 1250 hours, or about ten weeks. Divide he work with a couple of friends, and you can do it I thin a month on your spare cycles. "From what they tell" is a caveat, though. Those processes might need a Terabyte of RAM each.
Of course, all this would do (if their claim holds) is run for hours and print "Yes" or whatever that system prints when you ask it to prove that A implies A (Prolog afficiniados will feel at home)
Writing a formal proof in HOL Light is very much like writing a computer program. If the program run from start to finish without throwing errors, the proof is correct.
Writing a proof takes forever, because you have to take into account all possible corner cases etc, but I'd be surprised if running (hence: verifying) the entire Hale's proof would take more than a few minutes.
I'd be surprised if running (hence: verifying) the entire Hale's proof would take more than a few minutes.
I would have said the same thing before reading the announcement, but it says it took 5000 hours for some of the computations:
The term the_nonlinear_inequalities is defined as a conjection of several hundred nonlinear inequalities. The domains of these inequalities have been partitioned to create more than 23,000 inequalities. The verification of all nonlinear inequalities in HOL Light on the Microsoft Azure cloud took approximately 5000 processor-hours. Almost all verifications were made in parallel with 32 cores, hence the real time is about 5000 / 32 = 156.25 hours
Would those computations have to be repeated by every verifier? Or is theresome kind of certificate that can be verified faster?
This computationally intensive step is proving a bunch of inequalities originally calculated by floating point numerical routines. It does a software floating point emulation inside the theorem prover with proofs of bounds on the rounding at each step. Software floating point in an inefficient high-level language is slow!
If there was a certificate that could be verified faster, then that would be used as the proof instead. For now we're stuck with the ~900K lines of code and 5K cpu hours. I wouldn't be surprised if there's probably a lot of room for improvement, though.
A possible exception would be if the certificate was a probabilistic proof of some kind (someone mentioned the PCP theorem, which is an example of that), but I don't think mathematicians would be satisfied by that.
August 10, 2014 We are pleased to announce the completion of the Flyspeck project, which has constructed a formal proof of the Kepler conjecture. The Kepler conjecture asserts that no packing of congruent balls in Euclidean 3-space has density greater than the face-centered cubic packing. It is the oldest problem in discrete geometry. The proof of the Kepler conjecture was first obtained by Ferguson and Hales in 1998. The proof relies on about 300 pages of text and on a large number of computer calculations. [...]
I wonder if their proof process generated a certificate that would allow a single computer to verify their result in a reasonable amount of time?