A human-checkable proof of the 112-vertex counterexample to the Petersen coloring conjecture

Abstract

The Petersen coloring conjecture of Jaeger asserts that every bridgeless cubic graph admits a Petersen coloring. Recently, Putman presented an explicit counterexample on $112$ vertices and verified its non-colorability by showing, using a SAT solver, that an instance with $3640$ variables and $68324$ clauses is unsatisfiable. We give a short human-checkable proof that this graph is indeed a counterexample. Our proof determines the coloring behavior of the multipoles used in the construction by means of small explicit finite case analyses and reduces the final contradiction to a simple structural property of the line graph of the Petersen graph. Besides providing a proof that does not rely on a large SAT computation, our approach gives further insight into the gadgets underlying the construction.

Disclosure

“s work, the author used ChatGPT (OpenAI, GPT-5.6 Sol) for assistance with proofreading, improving the presentation and rewriting parts of the proofs, as well as with the preparation of figures and tables. The author critically reviewed all AI-assisted output and edited it where necessary. All mathematical statements, arguments, and proofs in this paper were independently verified by the author, who takes full responsibility for the correctness and content of the manuscript. References”

PDF page 6

Classification

Rewriting existing author-written text

Multiplier

4

Verified

2026-08-23T05:06:21.107193Z

Structural counts