5 ms·

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

100 points by andrewljohnson 12y ago

pera 12y ago
The Dense Sphere Packings book can be downloaded here: https://code.google.com/p/flyspeck/source/browse/trunk/kepler_tex/DenseSpherePackings.pdf https://code.google.com/p/flyspeck/source/browse/trunk/keple... (for some reason the link in the flyspeck project home is dead)
deleted 12y ago
[deleted]
kenko 12y ago
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 http://en.wikipedia.org/wiki/Oranges_Are_Not_the_Only_Fruit
- thret 12y ago
  Interesting spot to plug a book. Is it any good? My book list has been shrinking the last few months.
  - kenko 12y ago
    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.
bumbledraven 12y ago
https://code.google.com/p/flyspeck/wiki/AnnouncingCompletion 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?
- gghh 12y ago
  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.
  - bumbledraven 12y ago
    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?
    - murbard2 12y ago
      Indeed there is, http://en.wikipedia.org/wiki/PCP_theorem http://en.wikipedia.org/wiki/PCP_theorem
      - bumbledraven 12y ago
        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")
    - Strilanc 12y ago
      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.
cgh 12y ago
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.
krick 12y ago
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.
- Strilanc 12y ago
  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 http://youtu.be/DJx8bFQbHsA?t=40m57s
- sillysaurus3 12y ago
  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?
  - lutusp 12y ago
    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.
lutusp 12y ago
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.
- shasta 12y ago
  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.
  - lutusp 12y ago
    > 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."
    - gohrt 12y ago
      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-proof-checking-machine http://math.stackexchange.com/questions/324867/automated-pro...
      - colanderman 12y ago
        To be fair, n may be arbitrarily large, hence the undecidability of logics in general. (Not disagreeing with you, just clarifying.)
colanderman 12y ago
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.
- Steuard 12y ago
  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 http://en.wikipedia.org/wiki/Close-packing_of_equal_spheres)
  - colanderman 12y ago
    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.)
  - alok-g 12y ago
    Thank you. :-)
jeffdavis 12y ago
What is the definition of "efficient" in this context?
- colanderman 12y ago
  Packing density (i.e. ratio of fruits/spheres volume to unit volume).
colanderman 12y ago
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 http://en.wikipedia.org/wiki/Quasicrystal.

100 points by andrewljohnson 12y ago

pera 12y ago

The Dense Sphere Packings book can be downloaded here: https://code.google.com/p/flyspeck/source/browse/trunk/kepler_tex/DenseSpherePackings.pdf https://code.google.com/p/flyspeck/source/browse/trunk/keple... (for some reason the link in the flyspeck project home is dead)

deleted 12y ago

[deleted]

kenko 12y ago

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 http://en.wikipedia.org/wiki/Oranges_Are_Not_the_Only_Fruit

thret 12y ago
Interesting spot to plug a book. Is it any good? My book list has been shrinking the last few months.
- kenko 12y ago
  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.

bumbledraven 12y ago

https://code.google.com/p/flyspeck/wiki/AnnouncingCompletion 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?

gghh 12y ago
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.
- bumbledraven 12y ago
  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?
  - murbard2 12y ago
    Indeed there is, http://en.wikipedia.org/wiki/PCP_theorem http://en.wikipedia.org/wiki/PCP_theorem
    - bumbledraven 12y ago
      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")
  - Strilanc 12y ago
    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.

cgh 12y ago

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.

krick 12y ago

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.

Strilanc 12y ago
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 http://youtu.be/DJx8bFQbHsA?t=40m57s
sillysaurus3 12y ago
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?
- lutusp 12y ago
  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.

lutusp 12y ago

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.

shasta 12y ago
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.
- lutusp 12y ago
  > 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."
  - gohrt 12y ago
    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-proof-checking-machine http://math.stackexchange.com/questions/324867/automated-pro...
    - colanderman 12y ago
      To be fair, n may be arbitrarily large, hence the undecidability of logics in general. (Not disagreeing with you, just clarifying.)

colanderman 12y ago

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.

Steuard 12y ago
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 http://en.wikipedia.org/wiki/Close-packing_of_equal_spheres)
- colanderman 12y ago
  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.)
- alok-g 12y ago
  Thank you. :-)

jeffdavis 12y ago

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

colanderman 12y ago
Packing density (i.e. ratio of fruits/spheres volume to unit volume).

colanderman 12y ago

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 http://en.wikipedia.org/wiki/Quasicrystal.