OPG-401: circular chromatic number at most 20/7

Open

OPG401.root_problem

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

circular-coloringcombinatoricsgraph-theoryopen-problem

Let $G$ be any finite simple graph that is planar, triangle-free, and has maximum degree at most three. Then there exists a map $\varphi:V(G)\to\mathbb Z_{20}$ such that every edge has cyclic color distance between $7$ and $13$ :

7\le d_{20}(\varphi(u),\varphi(v))\le13 \qquad\text{for every }uv\in E(G).

Equivalently, every graph in the stated class has circular chromatic number at most $20/7$ . Disconnected and empty graphs are included.

Preamble

import Definitions.Def_opg401_circular_coloring

Formal statement

namespace OPG401

universe u

/-- OPG-401: every finite simple triangle-free planar subcubic graph has a
`(20,7)`-coloring. -/
theorem root_problem
    {V : Type u} [Fintype V] (G : SimpleGraph V)
    (hplanar : IsPlanar G) (htriangle : IsTriangleFree G)
    (hsubcubic : IsSubcubic G) :
    ∃ color : V → Fin 20, IsPQColoring G 20 7 color := by sorry

end OPG401

Source

Open Problem Garden / UnsolvedMath OPG-401, https://www.unsolvedmath.com/problems/OPG-401

Read-back

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

For a type V equipped with a Fintype instance, a simple graph G on V, and hypotheses that (i) there exists an injective map p : V → ℝ × ℝ such that no vertex distinct from both endpoints of an edge lies on the corresponding closed straight segment, and any two edges whose four endpoints are pairwise distinct have disjoint closed straight segments; (ii) for every a,b,c ∈ V, adjacency of a to b and b to c implies that c is not adjacent to a; and (iii) every vertex has at most three distinct neighbors, the declaration asserts that there exists a function color : V → Fin 20 such that for every edge u–v,

7 ≤ \min\bigl((color(u).val + 20 − color(v).val) \mathbin{\operatorname{mod}} 20,\ (color(v).val + 20 − color(u).val) \mathbin{\operatorname{mod}} 20\bigr) ≤ 20 − 7 = 13.

Here the first hypothesis uses the closed segment consisting of all points ((1 − t)x₁ + t y₁, (1 − t)x₂ + t y₂) with t ∈ ℝ and 0 ≤ t ≤ 1; the second and third hypotheses quantify over all vertices, including the possibility that V is empty. No uniqueness of the coloring is asserted.

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