That makes sense; it just happened that we tried the other identities after having written and submitted the paper. More importantly, the variants of Wilkie's identity we tried were suggested to us by an expert on the topic; I have just sent an email asking if they are okay with us sharing them, and if so I will post a link here.

> how big was the slowdown and how much less total clauses were there in that encoding? if I understand it correctly, that was still the biggest clause maker, but by how much?

It was roughly a factor of 8 fewer clauses, and yet over 5 times slower. If you're interested in the design of compact CNF encodings, and their effects on runtime, that's exactly the topic of my PhD thesis, and this proposal might give an initial idea: https://bsubercaseaux.github.io/assets/pdf/proposal.pdf

Naturally, there could be another encoding that has fewer clauses (say, O(n^5) or even O(n^4)) and does perform better in practice. But we didn't come up with one.

> also, have you tried reordering order of operations in symmetry break? how much did it affect the search?

To some extent. It was of moderate impact in terms of the runtime, but presumably the enumeration up to isomorphism would have been harder if we didn't consider the addition variables first. To have some updated numbers, I just ran some experiments with the 3! = 6 permutations of {A, M, E} on n=10.

AME (used in the paper) -> 92.7s AEM -> 110.8s MAE -> 139.4s MEA -> 157.4s EAM -> 297.1s EMA -> 276.8s

Note that it's not obvious at all how to search the space of possible exotic identities, so a potential direction for future work would be to have a loop in which LLMs (perhaps through something like AlphaEvolve) propose an exotic identity, and then a SAT call tries to find a small countermodel. A big issue though, is that even with our efficient encoding the SAT calls would take at least a few minutes, so we wouldn't be able to afford testing millions of candidates. But if there were 1000 candidates that could potentially be tested...

(I'm one of the authors of the paper, thanks for the coment!).

Personally, this is one of the cases with LLM-generated Lean that I feel most comfortable with: the proofs are all mathematically simple, and we included an example of correctness for one of the SAT constraints in the paper to show that there is nothing complicated about them. Writing them all in Lean, however, would be a very tedious task for which I see no particular benefit (i.e., it's not like some other formalization projects in which one learns something by formalizing; for an example of a human-written Lean correctness proof of a SAT encoding, you can check the paper https://arxiv.org/abs/2403.17370 in which I participated).

Regarding the byte-for-byte equality, the point is that we first had the Python code (which we wrote manually), and then asked LLMs to implement an encoder in Lean that would not only produce "equivalent" formulas but exactly equal formulas, meaning that it would use the same variable indices and the same clauses in the same order. It is well-known that such superficial factors (e.g., clause or variable ordering) can actually have large effects on solver performance (see https://www.cs.utexas.edu/~marijn/publications/pos18.pdf). The Python code is not part of the trust chain, and the Lean code does not rely on it in any way. We included the Python code in the repository since it's much shorter and easier to read.

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.

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.

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!

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.

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 :)

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...

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 :)

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...

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.

Comments URL: https://news.ycombinator.com/item?id=34660065

Points: 94

# Comments: 34

I originally didn't think it would get much attention, provided it's a bit technical...