7 ms·

The Packing Chromatic Number of the Infinite Grid is 15: the story behind it

94 points by bsubs 4y ago

bsubs 4y ago
In this blog post I tell my story working on a Math problem that I discovered in a Facebook Math group, and worked on for almost 3 years, until solving the problem and getting congratulated by my personal hero Don Knuth.
- runnerup 4y ago
  What a truly wonderful "blog post" to read! It feels like much more than a blog post. A whole very short story. I hope this reaches many, many people on HN. I wish I had read this in high school so that I better understood what ideal academia is all about.
- deleted 4y ago
  [deleted]
- tgv 4y ago
  Nicely written. It has a good balance between details and the larger picture.
jimmySixDOF 4y ago
>The solution to the problem took a total of 4851 CPU hours (we used a supercomputer with 128 cores!), and verifying the proof took another 4336 CPU hours. The total uncompressed proof weighed 122 terabytes! and only 34 terabytes after compression. It is easy to forget the scale at which academia operates.
- imiric 4y ago
  While certainly on the high end, those resources are available to consumers today. 128 cores and 122 TB of storage can be built relatively cheaply (or just rented from the cloud), and doesn't require what we traditionally considered exclusive to supercomputers. The scale of that would be in the order of thousands of cores and petabytes of storage.
- Jabbles 4y ago
  Are you suggesting that this is big or small? The "supercomputer" m6idn.32xlarge with 128 vCPU on AWS costs $1.3409 per Hour (spot pricing). So 9000 hours of compute would be ~$12k. https://aws.amazon.com/ec2/spot/pricing/ https://aws.amazon.com/ec2/spot/pricing/
  - deleted 4y ago
    [deleted]
  - sp332 4y ago
    It's very small. You could buy outright a pair of AMD Epyc CPUs with 64 cores each for less than that. Since transferring 36 TB of data out of AWS costs about $3,000, you can actually include the rest of the system including dual-CPU motherboard and tons of storage for $15,000.
LegionMammal978 4y ago
That's an impressively large counterexample for the chessboard conjecture! What prevents smaller counterexamples from existing? Is there some issue related to density, or is it pure coincidence?
- c7b 4y ago
  Not too familiar with this specific work, but it's not so uncommon in math that proofs are first found using some very large inputs that are then progressively simplified in further work. One prominent example would be prime gaps: in 2013 someone proved that there are infinitely many primes that are at most ~70 million apart, and in the following years that gap has successively dropped to 246 iirc (the goal remains getting it down to 2, of course). And there are some famous examples of far larger numbers, some too large to meaningfully represent in our physical universe, that have been used in proofs and then rendered obsolete by later work (eg Graham's number, Skewes' number). So (again, without knowing much about the problem at hand), the answer to your question might be that the simplest possible examples are much simpler anyway.
  - bsubs 4y ago
    Even though you're right in general, this is not the case here! We have proved that no smaller counter-example exists (again by using a computer search through optimized SAT-solving). As for the question of why no smaller counter-examples, I'm afraid I don't have any nice answers and perhaps there simply isn't a nice answer. Let me explain what I mean. My advisor Marijn Heule finished the resolution of Keller's conjecture (a conjecture about how N-dimensional cubes work in the Euclidean N-dimensional space), and the final answer is that the conjecture fails for the first time in dimension 8. "Why 8?" Again it's the same situation: it seems that that's just the way math is, something in the way the definitions and the objects behave makes it so that is the smallest counterexample. "Why" is a hard question to answer...
    - c7b 4y ago
      Oh wow, cool work! Yeah, the 'why' question can be hard to answer. We already have a proof that spells out a perfectly rigorous answer, but often we're looking for a 'deeper' connection to something perceived as more fundamental.
thaumasiotes 4y ago
The stated definitions of distance-coloring and standard coloring are incorrect; the protasis needs to specify that u ≠ v. As written, no coloring or distance-coloring of any graph can exist.
- bsubs 4y ago
  Thanks! silly omission on my side, will fix it now! Hopefully that didn't harm understanding!
thaumasiotes 4y ago
> At this point, we were conjecturing that using color in the chessboard pattern that yields density 1/2 was optimal, meaning that you could packing-color a graph D_r with k colors if, and only if, you could do it enforcing the chessboard pattern of 1's. > After more optimizations, it turned out the chessboard conjecture was false > Figure 19: The smallest counterexample to the chessboard conjecture. The diamond of radius 14, and a 6 forced in the center, can be packing-colored with 14 colors only if the chessboard pattern is broken. I don't understand why this is a counterexample to the conjecture. Painting the center with color 6 isn't part of the graph. Can the diamond of radius 14 be colored using a checkerboard pattern of 1s when the center color isn't 6? Is the diamond of radius 14, with a 2 forced in the center and in all 4 squares adjacent to the center, a counterexample to the conjecture that the infinite grid is colorable at all?
- penteract 4y ago
  > Can the diamond of radius 14 be colored using a checkerboard pattern of 1s when the center color isn't 6? Yes - the counterexample given can be shifted left by 1, making a the center color 1 (more 1s can be inserted completing the checkerboard pattern). I suspect that the conjecture to which this is a counterexample was imprecisely stated in the blog post, although there could also be a reason that a counterexample with a 6 in the center leads to a general counterexample.
  - bsubs 4y ago
    Thanks! this is a correct answer. Indeed I stated the conjecture a bit imprecisely in the blog post (the paper is more detailed in this respect). Just to make it fully precise, the conjecture was that if you take any $D_r$ graph, and force any color in the center (to avoid parity considerations that shift the chessboard pattern, assume the center color is different from $1$), then you can packing-color it if and only if you can do so after enforcing the chessboard pattern. In simpler words, the conjecture was that you could assume without loss of generality that the 1s would make a chessboard pattern, and this is not true in general. It is however likely that a modified version of the chessboard conjecture is true. In particular, Don Knuth thinks it holds for all diamonds of odd radius. There is a precise way of formalizing his variant of the conjecture. However, I'm not too inclined to work on it now that the core problem has been solved... About the "why 6 in the center?" implicit question in your comment: this is a nice question and I unfortunately only have a speculative answer (which is stated to some degree in the paper as we have an entire section on how to choose the center-color). In some sense, there's not really a way to answer this question super nicely: this is the smallest counter-example, and for some reason of the mathematical universe no smaller counter-example exists. I'm 90% sure that 6 is the smallest center-color for which a counter-example of this size exists. It's definitely possible to run 5 more experiments to confirm this, although given that it costs money to do so (even if neither me or my advisor are directly paying for the computing resources), I'm not sure if it's worth doing.
petters 4y ago
Are there some infinite graphs and k that only admit non-periodic solutions?
- bsubs 4y ago
  This is a question I've spent significant time on! (under a more technical formalization, of course) I've proved that this is not possible in infinite 1-dimensional graphs (like the infinite path, or an infinite grid of size C x Infinity, for a finite number C). For graphs that are infinite in two dimensions I don't have an answer yet (and it's likely that I never will). I'm very fond of this question tho, so if you give me your email (you can contact me at bsuberca@cs.cmu.edu), I can promise to write you back if at some future point in time I have a solution to this, or if someone else shares one with me :)
jxf 4y ago
There are a couple of technical typos in the post, but overall I found this a very cool and engaging read. It also reaffirms my belief that I find Coq neither fun nor readable (unlike Befunge which I find fun but unreadable, or Java, which I find readable but unfun). Congratulations, Bernardo!
- bsubs 4y ago
  Thanks jxf! I just fixed some, although it's likely that some typos remain. I agree with you about Coq, although there are some very smart folks working on it. My concern is that most of the improvements I've heard of are not about usability directly (i.e., how fun and readable it is to work with). I also don't quite now of precise low-hanging fruits that would improve it in this direction, but hopefully theorem provers will get friendlier and easier to use as time advances. Also the library of lemmas other people have proved and one can just plug in is steadily growing, so that should also reduce the pain of proving new stuff...
bcatanzaro 4y ago
This was an extremely enjoyable read, thanks to the author for taking the time to write this up.
- bsubs 4y ago
  Thanks to you for the feedback!! :) reading some positive comments here has definitely paid off the investment of time in writing the post and taking care of the figures (by far the most time-consuming part haha).
  - bcatanzaro 4y ago
    The figures are beautiful!
deleted 4y ago
[deleted]

94 points by bsubs 4y ago

In this blog post I tell my story working on a Math problem that I discovered in a Facebook Math group, and worked on for almost 3 years, until solving the problem and getting congratulated by my personal hero Don Knuth.

runnerup 4y ago
What a truly wonderful "blog post" to read! It feels like much more than a blog post. A whole very short story. I hope this reaches many, many people on HN. I wish I had read this in high school so that I better understood what ideal academia is all about.
deleted 4y ago
[deleted]
tgv 4y ago
Nicely written. It has a good balance between details and the larger picture.

jimmySixDOF 4y ago

>The solution to the problem took a total of 4851 CPU hours (we used a supercomputer with 128 cores!), and verifying the proof took another 4336 CPU hours. The total uncompressed proof weighed 122 terabytes! and only 34 terabytes after compression. It is easy to forget the scale at which academia operates.

imiric 4y ago
While certainly on the high end, those resources are available to consumers today. 128 cores and 122 TB of storage can be built relatively cheaply (or just rented from the cloud), and doesn't require what we traditionally considered exclusive to supercomputers. The scale of that would be in the order of thousands of cores and petabytes of storage.
Jabbles 4y ago
Are you suggesting that this is big or small? The "supercomputer" m6idn.32xlarge with 128 vCPU on AWS costs $1.3409 per Hour (spot pricing). So 9000 hours of compute would be ~$12k. https://aws.amazon.com/ec2/spot/pricing/ https://aws.amazon.com/ec2/spot/pricing/
- deleted 4y ago
  [deleted]
- sp332 4y ago
  It's very small. You could buy outright a pair of AMD Epyc CPUs with 64 cores each for less than that. Since transferring 36 TB of data out of AWS costs about $3,000, you can actually include the rest of the system including dual-CPU motherboard and tons of storage for $15,000.

LegionMammal978 4y ago

That's an impressively large counterexample for the chessboard conjecture! What prevents smaller counterexamples from existing? Is there some issue related to density, or is it pure coincidence?

c7b 4y ago
Not too familiar with this specific work, but it's not so uncommon in math that proofs are first found using some very large inputs that are then progressively simplified in further work. One prominent example would be prime gaps: in 2013 someone proved that there are infinitely many primes that are at most ~70 million apart, and in the following years that gap has successively dropped to 246 iirc (the goal remains getting it down to 2, of course). And there are some famous examples of far larger numbers, some too large to meaningfully represent in our physical universe, that have been used in proofs and then rendered obsolete by later work (eg Graham's number, Skewes' number). So (again, without knowing much about the problem at hand), the answer to your question might be that the simplest possible examples are much simpler anyway.
- bsubs 4y ago
  Even though you're right in general, this is not the case here! We have proved that no smaller counter-example exists (again by using a computer search through optimized SAT-solving). As for the question of why no smaller counter-examples, I'm afraid I don't have any nice answers and perhaps there simply isn't a nice answer. Let me explain what I mean. My advisor Marijn Heule finished the resolution of Keller's conjecture (a conjecture about how N-dimensional cubes work in the Euclidean N-dimensional space), and the final answer is that the conjecture fails for the first time in dimension 8. "Why 8?" Again it's the same situation: it seems that that's just the way math is, something in the way the definitions and the objects behave makes it so that is the smallest counterexample. "Why" is a hard question to answer...
  - c7b 4y ago
    Oh wow, cool work! Yeah, the 'why' question can be hard to answer. We already have a proof that spells out a perfectly rigorous answer, but often we're looking for a 'deeper' connection to something perceived as more fundamental.

thaumasiotes 4y ago

The stated definitions of distance-coloring and standard coloring are incorrect; the protasis needs to specify that u ≠ v. As written, no coloring or distance-coloring of any graph can exist.

bsubs 4y ago
Thanks! silly omission on my side, will fix it now! Hopefully that didn't harm understanding!

thaumasiotes 4y ago

> At this point, we were conjecturing that using color in the chessboard pattern that yields density 1/2 was optimal, meaning that you could packing-color a graph D_r with k colors if, and only if, you could do it enforcing the chessboard pattern of 1's. > After more optimizations, it turned out the chessboard conjecture was false > Figure 19: The smallest counterexample to the chessboard conjecture. The diamond of radius 14, and a 6 forced in the center, can be packing-colored with 14 colors only if the chessboard pattern is broken. I don't understand why this is a counterexample to the conjecture. Painting the center with color 6 isn't part of the graph. Can the diamond of radius 14 be colored using a checkerboard pattern of 1s when the center color isn't 6? Is the diamond of radius 14, with a 2 forced in the center and in all 4 squares adjacent to the center, a counterexample to the conjecture that the infinite grid is colorable at all?

penteract 4y ago
> Can the diamond of radius 14 be colored using a checkerboard pattern of 1s when the center color isn't 6? Yes - the counterexample given can be shifted left by 1, making a the center color 1 (more 1s can be inserted completing the checkerboard pattern). I suspect that the conjecture to which this is a counterexample was imprecisely stated in the blog post, although there could also be a reason that a counterexample with a 6 in the center leads to a general counterexample.
- bsubs 4y ago
  Thanks! this is a correct answer. Indeed I stated the conjecture a bit imprecisely in the blog post (the paper is more detailed in this respect). Just to make it fully precise, the conjecture was that if you take any $D_r$ graph, and force any color in the center (to avoid parity considerations that shift the chessboard pattern, assume the center color is different from $1$), then you can packing-color it if and only if you can do so after enforcing the chessboard pattern. In simpler words, the conjecture was that you could assume without loss of generality that the 1s would make a chessboard pattern, and this is not true in general. It is however likely that a modified version of the chessboard conjecture is true. In particular, Don Knuth thinks it holds for all diamonds of odd radius. There is a precise way of formalizing his variant of the conjecture. However, I'm not too inclined to work on it now that the core problem has been solved... About the "why 6 in the center?" implicit question in your comment: this is a nice question and I unfortunately only have a speculative answer (which is stated to some degree in the paper as we have an entire section on how to choose the center-color). In some sense, there's not really a way to answer this question super nicely: this is the smallest counter-example, and for some reason of the mathematical universe no smaller counter-example exists. I'm 90% sure that 6 is the smallest center-color for which a counter-example of this size exists. It's definitely possible to run 5 more experiments to confirm this, although given that it costs money to do so (even if neither me or my advisor are directly paying for the computing resources), I'm not sure if it's worth doing.

petters 4y ago

Are there some infinite graphs and k that only admit non-periodic solutions?

bsubs 4y ago
This is a question I've spent significant time on! (under a more technical formalization, of course) I've proved that this is not possible in infinite 1-dimensional graphs (like the infinite path, or an infinite grid of size C x Infinity, for a finite number C). For graphs that are infinite in two dimensions I don't have an answer yet (and it's likely that I never will). I'm very fond of this question tho, so if you give me your email (you can contact me at bsuberca@cs.cmu.edu), I can promise to write you back if at some future point in time I have a solution to this, or if someone else shares one with me :)

jxf 4y ago

There are a couple of technical typos in the post, but overall I found this a very cool and engaging read. It also reaffirms my belief that I find Coq neither fun nor readable (unlike Befunge which I find fun but unreadable, or Java, which I find readable but unfun). Congratulations, Bernardo!

bsubs 4y ago
Thanks jxf! I just fixed some, although it's likely that some typos remain. I agree with you about Coq, although there are some very smart folks working on it. My concern is that most of the improvements I've heard of are not about usability directly (i.e., how fun and readable it is to work with). I also don't quite now of precise low-hanging fruits that would improve it in this direction, but hopefully theorem provers will get friendlier and easier to use as time advances. Also the library of lemmas other people have proved and one can just plug in is steadily growing, so that should also reduce the pain of proving new stuff...

bcatanzaro 4y ago

This was an extremely enjoyable read, thanks to the author for taking the time to write this up.

bsubs 4y ago
Thanks to you for the feedback!! :) reading some positive comments here has definitely paid off the investment of time in writing the post and taking care of the figures (by far the most time-consuming part haha).
- bcatanzaro 4y ago
  The figures are beautiful!

deleted 4y ago

[deleted]