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...
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).
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 :)
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...
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.
I agree, and it would be amazing for someone to find a deeper intuitive reason for why 15 is the answer to this problem, or 8 is the answer to that other problem, or many such cases.
This is however extremely hard in my opinion (note that I say "opinion" on purpose, because I don't have any way to formalize this idea). Let me use a couple more examples: any Rubik's cube (3x3x3) can be solved in at most 20 moves (on the standard metric, counting double turns as one move), and a Sudoku needs at least 17 clues to have a unique solution. Why 20? Why 17? We (humanity) got to both answers through computation, and even though the computation requires mathematical observations to be made more efficient, at the end we still checked an in-human number of cases... So in all honesty, if I had to bet, I'd say we will probably never intuitively know why 20 moves or why 17 clues, or in my case, why 15 colors... I'd love to be proven wrong tho!
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.
> 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
I'm interested in the conjecture that was stated in the post. That one just says "if a k-coloring exists, then a k-coloring in which the 1s form a perfect checkerboard pattern also exists".
That seems like it's enough to allow you to assume without loss of generality that the 1s form a checkerboard pattern. That's still a huge reduction in the search space - you need to consider that the pattern might be shifted, but that only doubles the amount of work you're doing (since there are only two ways to fill in a checkerboard pattern on a grid), while filling in the checkerboard cuts the amount of work you're doing by a factor of 2^k.
Also, it seems like something of an "error" (maybe not! What do we know about aperiodic colorings?) when thinking about checkerboarding to spend time considering graphs that won't tile the plane. The radius-14 diamond can't tile the plane while checkerboarded; a checkerboard pattern will hit more or less than half of the cells in the grid.
Let me be a bit more precise here (at risk of being pedantic) to make sure we're on the same page. (Also, if you have a concrete idea of how to reformulate the text so this is clearer, I'm definitely interested!)
Here are two well-defined conjectures:
Conjecture 1. A packing-coloring of the infinite square grid exists using colors {1, ..., k} if, and only if, there exists one with a chessboard pattern (meaning that wlog all vertices (a, b) such that a+b is odd get color 1).
Conjecture 2. Let $D_{r, k, c}$ be the instance consisting of whether $D_r$ can be packing-colored with $k$ colors assuming it gets color $c$ in the center. Then enforcing that all vertices (a, b) such a+b is odd get color 1 does not change the satisfiability of the instance.
Conjecture 1 is true, based on our paper: if k <= 14, then no packing-coloring exists anyway, so the conjecture is vacuously true. If k >= 15, then we know of a packing-coloring that respects the chessboard pattern (the one in Figure 12), and so the conjecture holds.
Conjecture 2 is false, this is where the smallest counterexample in the post kicks in.
Note that given that 13 colors are not enough, we knew that if there was a solution with 14 colors, it must use color 6 somewhere, and by restricting ourselves to $D_{14}$ around such a vertex, we run into the issue!
About your last comment, we use diamond graphs to prove lower bounds (i.e., that a certain number of colors is not enough), while finite square grids are used to prove upper bounds (as in Figure 12).
About aperiodic colorings, see the other comment in this thread were we discuss about it a bit :)
> Conjecture 1. A packing-coloring of the infinite square grid exists using colors {1, ..., k} if, and only if, there exists one with a chessboard pattern (meaning that wlog all vertices (a, b) such that a+b is odd get color 1).
I understand this, but I'll need to refer to it in a moment...
> Conjecture 2. Let $D_{r, k, c}$ be the instance consisting of whether $D_r$ can be packing-colored with $k$ colors assuming it gets color $c$ in the center. Then enforcing that all vertices (a, b) such a+b is odd get color 1 does not change the satisfiability of the instance.
I'll assume that D_r refers to a taxicab disc ("diamond") of radius r?
Conjecture 2 is well-defined, but I see several problems with it. Conjecture 1 seems like a reasonable thing to investigate (though it's not what I had in mind); Conjecture 2 doesn't.
Most obviously, Conjecture 2 is false, since D_{r, k, 1} is dramatically affected by forcing all cells at an odd taxicab distance from the center to take color 1.
Second, while you are correct to say that the existence of any checkerboard pattern which successfully k-colors the infinite grid implies the existence of a checkerboard pattern which k-colors the infinite grid and assigns color 1 to those vertices (a, b) such that a+b is odd, the same cannot be said (and you haven't said it) about a finite grid. It it then not obvious why, when discussing a finite grid, you want to restrict checkerboard patterns to those which assign color 1 to vertices at an odd taxicab distance from the center of the grid. You can't say "without loss of generality" about that choice; the grid is no longer infinite. In your 14-diamond, this presents the problem that the off-center checkerboard cannot color half of the cells in the grid, because -- to use a chessboard analogy -- the number of "black" cells is not equal to the number of "white" cells. This suggests an obvious reason why a checkerboard that is forced to color the smaller half of the diamond might prove to be inadequate to the task.
Third, it is not obvious why you want to restrict yourself to grids that have a center cell. The following grid is not a taxicab disc:
xxxxxx
xxxxxx
xxxxxx
xxxxxx
xxxxxx
xxxxxx
But it can be colored and it can be given a checkerboard pattern. And unlike a diamond, it can be used to tile the infinite grid with its checkerboard pattern intact.
The question I'm really asking here is, I guess, "What is the point of your Conjecture 2? Who would care what the answer was?" You introduced it as a way to cut down on the search space for a computationally-intensive trial-and-error problem, and it appears to be effective at that goal. But you go on to say that you can't use it to achieve that goal because it's false, when a version of your conjecture that is (1) much more natural to pose; and (2) equally useful for the purpose of cutting the search space, might still be true! You wouldn't want the checkerboard to avoid the center of a diamond anyway, because if it goes through the center of the diamond, it will give you a bigger reduction in the search space than the checkerboard that avoids the center will!
Why is the conjecture not this one?
Checkerboard Conjecture: for any "interesting subset" [Diamonds on the grid? Bounded convex subsets of the grid? Connected subsets? This can be refined; maybe diamonds are fine.] of the infinite grid ℤ², if any packing-coloring exists with k colors, then a packing-coloring exists with k colors in which color 1 forms a checkerboard. That is to say, any two vertices v = (a, b) and w = (c, d) satisfy a+b ≡ c+d (mod 2) if and only if (either v and w both have color 1, or v and w both fail to have color 1).
I think I see what you mean, but it seems to me that you're mixing ideas about the chessboard conjecture in this particular context, with more general versions of the conjecture (a bunch of which we don't know the answer for, and might be interesting in their own right).
In particular, to show that the packing-chromatic number of the infinite grid is 15, we needed to find a finite subgraph of the infinite square grid for which 14 colors are not enough. The class of sub-graphs that seemed more amenable to do this was that of diamonds (i.e., disks in the corresponding metric) of radius r. If you simply try to determine whether D_{14} can be packing-colored with 14 colors, that instance is too hard, so we make it easier by forcing a color in the center (this is a form of symmetry breaking). Forcing the center to take color 1 is the worst possible choice (see Fig 6. of the paper https://arxiv.org/pdf/2301.09757v1.pdf), therefore we want to force it to something other than 1, let's say 6 (this seems to be the best choice in practice).
Your problem then reduces to determine whether D_{14} can be packing-colored with 14 colors, when forcing a 6 in the center. It turns out again that this is not easy enough to solve naively, so it would be really nice it we could assume without loss of generality that we can enforce the chessboard pattern as well as the 6 in the center (which given that the center has even coordinates, it would imply that the 1s are at odd coordinates). I try to prove this manually and failed. But we ran the experiment assuming the conjecture to be true, and effectively there is no packing-coloring for D_{14} with 14 colors, a 6 in the center, and 1s in every odd coordinate. If Conjecture 2 had been true, then we would have ended our work there, but then we realize we couldn't assume Conjecture 2: we found a way of packing-coloring D_{14} with a 6 in the center when removing the chessboard assumption.
So the formalization in our context that made the most sense was: "is it true that given any radius r, any value of k, and any value of c, the forced center color, we can assume the chessboard pattern?" (Noting that if the center is forced to 1 as you mention in your comment, then the chessboard pattern would be 1s on the even coordinates).
This is what I meant with Conjecture 2, so hopefully now it's clear why it was of interest for this particular problem. It's not obvious at all that Conjecture 2 is false provided this! unless you have a new argument I'm unaware of!
Your last question is of course interesting, and many variations of the conjecture make sense and could be studied; we didn't really pose Conjecture 2 thinking it was the most interesting formulation, but rather a sufficiently simple one that would have justified our result of (D_{14}+6 in the center + 1s at odd coordinates)-is-not-packing-colorable-with-14-colors to imply the final result.
> that instance is too hard, so we make it easier by forcing a color in the center (this is a form of symmetry breaking)
The example of symmetry breaking in your post is "the instance of the largest color that appears closest to the center must appear in octant II".
I can understand this - by using a combination of rotations and reflections, any coloring that doesn't satisfy this constraint can be transformed into one that does. So the patterns we reject by using this "symmetry-breaking" approach are those that are identical, through one or more symmetries, to a pattern we won't reject. So far so good.
But forcing a color in the center can't be symmetry-breaking in this sense. Every symmetry of the diamond will map the center onto itself, so applying a "symmetry-breaking" rule that the center must be painted a particular color will let you rule out a total of zero patterns that can be transformed into patterns that match your rule. That is, literally, worthless.
Such a constraint will let you rule out patterns that aren't transformable into the patterns you do consider... but that's bad, not good.
What do you mean when you say that forcing a color in the center is a form of symmetry breaking?
Assume you know that 13 colors aren't enough and you want to prove that 14 aren't enough either. Any 14 packing-coloring of the grid must use color 6 somewhere, as otherwise it would be only using 13 colors that are no better than colors {1, ..., 13}, and thus not enough. Now, you can imagine the diamond you're considering is centered around one of these 6s. This is breaking a different kind of symmetry; a translational one, as it's breaking the original symmetry of centering your diamond on any possible color, by choosing an arbitrary one. Granted, this is different form of symmetry-breaking as it's not about auto-morphisms on the set of solution. Also, it's totally possible that "symmetry breaking" was a bad choice of words; as long as you agree that it's a helpful idea as it significantly reduces the search space, we are on the same page.
formalizing this might be tricky, I mean something like a bijection from (the set of mappings from an infinite packing-coloring to a fixed colored sub-graph) to itself.
> Any 14 packing-coloring of the grid must use color 6 somewhere, as otherwise it would be only using 13 colors that are no better than colors {1, ..., 13}, and thus not enough. Now, you can imagine the diamond you're considering is centered around one of these 6s. This is breaking a different kind of symmetry; a translational one
This is a good point; I had been thinking of the problem differently.
In this model, the diamond is viewed as just being a window onto the infinite grid, and we're not interested in whatever properties it might have considered as a finite graph. Thinking about it this way, the idea that the coloring in your article disproves is that "there is a 14-packing-coloring of the infinite grid which uses a chessboard pattern for color 1".
But then, since (by your later result) there is no 14-packing-coloring of the infinite grid, it's not too surprising that there isn't such a coloring that also features a chessboard.
What bothers me in this discussion of the chessboard conjecture is the switch: you say "at this point, we were conjecturing that using color 1 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". And this seems plausible, and the illustration provided as a counterexample isn't actually a counterexample to this statement. You can packing-color the graph shown there with 14 colors, and you can do so while enforcing the chessboard pattern of 1s.
In your explanation here, you're viewing D_r as a subgraph of the successfully-colored infinite grid, not as a finite graph in its own right. That handily explains why the chessboard pattern goes around the center of D_r instead of through it. The illustration in the post does then show that there's a problem. But to my eye, the problem is in the premise of a successfully 14-packing-colored infinite grid, not in the chessboard conjecture. In between stating the chessboard conjecture and providing the counterexample, you changed what the chessboard conjecture said -- there is no reference to the infinite grid in your statement of the chessboard conjecture, but the illustration of a "counterexample" is a counterexample to a statement about the infinite grid. It feels wrong. :-/
I see what you’re saying, but note that as mentioned above I did edit the post based on your feedback to be precise, stating that the conjecture we disproved was that regardless of the center color the chessboard of 1s could be assumed wlog in any finite diamond . (Also this is stated correctly in the paper, which at the end is the “source of truth”)
I agree with you that just saying “D_r can be colored with k colors iff it can be done with a chessboard pattern of 1s” is a slightly different statement to which our counterexample is not a counterexample, but I think you got trapped into my initial omission in the blog post, which was a writing mistake rather a mathematical mistake. I don’t think there’s anything wrong here, but sorry for the original version of this post being sloppy in the writing.
I agree again with what you were saying some messages ago about how versions of the conjecture that do not consider the center color can be more mathematically interesting. A proof that D_r can be colored with k colors iff it can be done with the chessboard pattern would definitely be super nice.
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.
