OPG-37271: six colors for every finite subcubic graph

Open

OPG37271.root_problem

by hao jia · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsedge-coloringgraph-theoryopen-problem

Let $G$ be any finite simple graph whose maximum degree is at most three. The problem asks for a star edge coloring of $G$ with six colors:

\Delta(G)\le 3 \quad\Longrightarrow\quad \chi'_s(G)\le 6.

The quantifier includes disconnected and empty graphs as well as graphs with vertices of degree below three. A star edge coloring is proper and forbids every bichromatic simple path or cycle of four edges; the paths need not be induced.

Preamble

import Definitions.Def_opg37271_star_edge_coloring

Formal statement

namespace OPG37271

universe u

/-- OPG-37271: every finite simple graph of maximum degree at most three has
a star edge coloring with six colors. -/
theorem root_problem
    {V : Type u} [Fintype V] (G : SimpleGraph V)
    (hsubcubic : IsSubcubic G) :
    HasStarEdgeColoring G 6 := by sorry

end OPG37271

Source

Open Problem Garden, OPG-37271, https://www.openproblemgarden.org/comment/reply/37271; Conjecture 1.4 in Lei--Shi--Song, Star chromatic index of subcubic multigraphs, J. Graph Theory 88 (2018), 566--576, https://arxiv.org/abs/1701.04105v3

Read-back

What the Lean code literally says, in plain math · gpt-5.6-luna

For every finite type of vertices $V$ , every simple graph $G$ on $V$ , and every hypothesis that each vertex has neighbor-set cardinality at most $3$ ,

\forall v\in V,\quad \operatorname{encard}(\operatorname{NeighborSet}_G(v))\le 3,

there exists an edge-coloring $c$ of $G$ using the six colors $\operatorname{Fin}(6)$ such that: (i) whenever $v,u,w\in V$ , $v$ is adjacent to both $u$ and $w$ , and $u\ne w$ , the colors assigned to the edges $vu$ and $vw$ are different; (ii) there do not exist pairwise distinct vertices $v_0,v_1,v_2,v_3,v_4$ with consecutive adjacencies $v_0v_1,v_1v_2,v_2v_3,v_3v_4$ such that the colors of $v_0v_1$ and $v_2v_3$ are equal and the colors of $v_1v_2$ and $v_3v_4$ are equal; and (iii) there do not exist pairwise distinct vertices $v_0,v_1,v_2,v_3$ with cyclic adjacencies $v_0v_1,v_1v_2,v_2v_3,v_3v_0$ such that the colors of $v_0v_1$ and $v_2v_3$ are equal and the colors of $v_1v_2$ and $v_3v_0$ are equal.

Human review

Endorsed by Shuze Chen · Sep 7, 2026
Endorsed by hao jia · Sep 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph