Proof confirmed of 400-year-old fruit-stacking problem | Hacker News Reader

Proof confirmed of 400-year-old fruit-stacking problem

newscientist.com

100 pointsandrewljohnson31 comments

https://code.google.com/p/flyspeck/wiki/AnnouncingCompletion

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?

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.

Indeed there is, http://en.wikipedia.org/wiki/PCP_theorem

I suppose I was unclear. I should have asked, is the file ready for me to download? (Not, "does such a certificate exist, in the platonic sense")

Note that it was already known that FCC was the best periodic packing (740‰ density); this was proven by Gauss. What was not known was whether there was a more efficient aperiodic packing, such as those described in http://en.wikipedia.org/wiki/Quasicrystal.

There is a good popular math book about Kepler's Conjecture: "Kepler's Conjecture: How Some of the Greatest Minds in History Helped Solve One of the Oldest Math Problems in the World", by George Szpiro. I enjoyed it and recommend it if you want a historical perspective on this problem.

I'm not saying that proof is bad or result isn't result enough, or that computer cannot help with math research — that would be ridiculous to say. But I strongly feel that all the news these days about results like this one are something that could be called either "overreaction" or "misunderstanding". Using computer to brute-force through hypothesis might be useful, and works like Voevodsky's one are both cool and useful, but when something like that becomes overrated it seems kinda sad to me.

"Machines do the grunt work and leave humans free for deeper thinking", really? Let me put it this way: what is the most important thing about, say, Pythagorean theorem? From the engineer's point of view it could be ability to find the length of the side of right triangle given the other two or something like that. From the mathematical point of view the most important thing about that or any other theorem is its proof. It isn't actually that important that you cannot divide arbitrary angle by 3 equal parts using only compass and the ruler — the way how you prove it is what really matters.

So, once again, autoverifiers are wonderful and so on, but if someone thinks that writing incomprehensible, but correct proofs is as fine as it gets — it's huge mistake to think so. Math is not about constructing and computing, it is about understanding in the first place.

This was far more than a brute force search. Thomas Hales did a talk about the proof and during the QA he mentioned that the proof was improved a lot as part of formalizing it into HOL. The process even lead to solutions of other problems [1].

1: http://youtu.be/DJx8bFQbHsA?t=40m57s

The four color theorem was proved by brute forcing every possible contradiction with a computer and finding that no contradiction existed. Therefore the four color theorem was proved to be true. Why is that a problem?

At the time, the problem was that most reviewers couldn't understand the code that produced the result, so they felt that they were accepting a result they couldn't meaningfully review or independently confirm.

A lesser issue was philosophical -- it didn't seem like mathematics was "supposed" to be conducted. This second issue has pretty much evaporated in the intervening years.

> but if someone thinks that writing incomprehensible but correct proofs is as fine as it gets — it's huge mistake to think so.

In the brute force case, it's simply a conceit of mathematicians that algorithms implemented in a programming language are incomprehensible. If our proofs can span hundreds of pages, why not also our programs?

Accepting the premise that large algorithms and their results can be used as part of a proof, have you ever proven a program correct by hand? It's almost always tedious and unenlightening.

The image on the sidebar is captioned "Oranges are not the only stacking fruit", which is ... interesting.

http://en.wikipedia.org/wiki/Oranges_Are_Not_the_Only_Fruit

Interesting spot to plug a book. Is it any good? My book list has been shrinking the last few months.

I have no idea! I've never read it, but it has a memorable title. The weird allusion can't have been accidental, though it is pretty strange.

The Dense Sphere Packings book can be downloaded here: https://code.google.com/p/flyspeck/source/browse/trunk/keple...

(for some reason the link in the flyspeck project home is dead)

I was surprised that face-centered cubic was the winner; I would have thought hexagonal close-packed would be; but the Internet tells me they have identical density, which blows my mind.

If you were to sit down with a pile of beads and try to build a big HCP stack and a big FCC stack layer by layer, you'd quickly understand why the densities are the same. The bottom two layers (call them A and B) are identical between the two (without loss of generality), but you then have two distinct ways to proceed.

For HCP, you shift back and add a layer identical to A (that is, the beads of the third layer are directly above the beads of the first) and then repeat, making an ABABAB... pattern. For FCC, you shift to the one allowed position that is not identical to A, making an ABCABC... pattern. (Fig. 1 of this Wikipedia article is at least a little useful for visualizing this: http://en.wikipedia.org/wiki/Close-packing_of_equal_spheres)

Moreso I think what throws me is that in your example, the FCC cubes are tilted. (i.e. if you build a FCC stack starting with a grid of squares rather than triangles, it's much more difficult to visualize where the closely-packed triangles lay.)

Thank you. :-)

What is the definition of "efficient" in this context?

Packing density (i.e. ratio of fruits/spheres volume to unit volume).

Quote: " ... this provides a foundation which ensures the computer can check any series of logical statements to confirm they are true." (emphasis added)

Not really. I wonder if the author of the linked article realizes that the Turing Halting Problem, and Gödel's incompleteness theorems, are deeply connected and prevent the claimed outcome as stated.

1. Checking a series of logical statements (a proof) is obviously decidable; it's a mere exercise in syntactic manipulation. This is exactly what Isabelle/HOL/Coq/Agda/etc. do.

2. Yes, the validity of theorems is undecidable. But even if that's what the quote was talking about (it's not, read the context), confirming truth (soundness) is very much something computers are capable of. Correctly deciding truth or falsity (soundness + completeness) is what is not possible in every case.

The quote pretty obviously is referring to checking a proof (series of logical statements) not an arbitrary logical statement. Compared to most reporting on technical subjects, this reporting was wonderful.

> The quote pretty obviously is referring to checking a proof (series of logical statements) not an arbitrary logical statement.

Checking a series of logical statements, and generating a series of logical statements, are not fundamentally different with respect to the issue of undecidability.

> Compared to most reporting on technical subjects, this reporting was wonderful.

Until I got to the passage I quoted, I agreed completely, and I agree in general in spite of it. It's one of those often-heard statements that make more experienced readers say, "Umm, wait, you really don't want to say it that way."

Checking a series of logical statements is just arithmetic.

Generating a series of logical statements is only hard because the formal statements are not generated axiomatically, they are sourced from ill-understood human creativity. Once a formalism is defined it is trivial O(e^n) algorithm to generate all proofs of size n.

http://math.stackexchange.com/questions/324867/automated-pro...

To be fair, n may be arbitrarily large, hence the undecidability of logics in general. (Not disagreeing with you, just clarifying.)

Reply on news.ycombinator.com