The paper tackles a classic question in graph theory: what is the smallest graph that requires four colors to color (no two adjacent vertices the same color) while also having no short cycles? Specifically, it focuses on graphs where every cycle has length at least six. The minimum number of vertices such a graph can have is called n(4,6), and pinning down its exact value is a long-standing open problem. Before this work, the best known bounds were that the answer lies somewhere between 26 and 66 vertices, with the 66-vertex example having stood as the record for several years.
The authors make progress on both ends of this range. They construct an explicit 64-vertex graph that needs four colors and has no cycles shorter than six, lowering the upper bound by two. This graph has a high degree of internal symmetry and is "critical" in the sense that removing any vertex or edge drops the coloring requirement to three. On the other side, they use a combination of computational search and mathematical reasoning to push the lower bound up to 29, meaning no such graph can exist with fewer than 29 vertices. The search uses a modern technique called SAT modulo symmetries, which cleverly avoids redundant work by exploiting the symmetry of the problem, and draws on a known result about how dense four-critical graphs must be.
Beyond these numerical improvements, the paper systematically rules out many structural forms a potential smaller example could take. For instance, no highly symmetric graphs built from group-theoretic constructions (Cayley graphs or those with small numbers of symmetry orbits) on 54 to 63 vertices can work. Since all previous record-setting graphs in this family were built using exactly such symmetric constructions, this closes off the most natural avenues for finding a smaller example below 64 vertices. Importantly, all the results including the proof that the new graph genuinely needs four colors have been formally verified using the Lean 4 proof assistant, providing an unusually high level of certainty for a computer-assisted result.