# The Packing Chromatic Number of the Infinite Square Grid is 15

arXiv: https://arxiv.org/abs/2301.09757 · HTML: https://mlsanity.com/paper/2301.09757/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 1 of its 27 references that are in the map.
- First posted on arXiv 23 Jan 2023.

## Builds on (most cited first, 1 of 1)

- [The DRAT format and DRAT-trim checker](https://mlsanity.com/paper/1610.06229/) (2016)

## Built on by (most cited first, 4 of 4)

- [Why should we ever automate moral decision making?](https://mlsanity.com/paper/2407.07671/) (2024)
- [Artifical intelligence and inherent mathematical difficulty](https://mlsanity.com/paper/2408.03345/) (2024)
- [Asymptotically Smaller Encodings for Graph Problems and Scheduling](https://mlsanity.com/paper/2506.14042/) (2025)
- [Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery](https://mlsanity.com/paper/2604.21187/) (2026)

## Abstract (arXiv)

A packing k-coloring is a natural variation on the standard notion of graph k-coloring, where vertices are assigned numbers from 1, ldots, k, and any two vertices assigned a common color c ∈ 1, ldots, k need to be at a distance greater than c (as opposed to 1, in standard graph colorings). Despite a sequence of incremental work, determining the packing chromatic number of the infinite square grid has remained an open problem since its introduction in 2002. We culminate the search by proving this number to be 15. We achieve this result by improving the best-known method for this problem by roughly two orders of magnitude. The most important technique to boost performance is a novel and surprisingly effective propositional encoding. Additionally, we developed a new symmetry-breaking method. Since both new techniques are more complex than existing techniques for this problem, a verified approach is required to trust them. We include both techniques in a proof of unsatisfiability, reducing the trusted core to the correctness of the direct encoding.