A planar graph without four- or nine-cycles that is not three-colorable

Lu, Wang, Wang, Bu, Montassier and Raspaud asked which cycle lengths, together with length four, force proper three-colorability of planar graphs, as recorded by Kang, Jin and Wang. Cohen-Addad, Hebdige, Král', Li and Salgado disproved Steinberg's conjecture for lengths four and five. Kostochka and Yancey proved a sharp general lower bound on the number of edges of a four-critical graph. We give an 82-vertex planar graph without cycles of length four or nine that is four-critical and attains that bound, answering the length-nine case of that question. The graph is obtained by Dirac–Hajós–Gallai–Ore compositions of complete four-vertex graphs. Its non-three-colorability follows by induction on this construction; a rotation system, cycle enumeration and three-colorings after edge deletion establish the remaining properties. Lean verifies the rotation certificate, the exclusion of four- and nine-cycles, and non-three-colorability of the same graph.

Checked in Lean from the definitions; not yet reviewed by experts. Produced by AI models under the author's direction.