OPG-169: the Two Color Conjecture for planar digraphs

Open

OPG169.root_problem

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

combinatoricsdirected-graphsgraph-theoryopen-problemplanar-graphs

For every orientation $D$ of a finite simple planar graph, there exists a vertex coloring $c:V(D)\to\{0,1\}$ such that both full induced color classes are acyclic:

D[c^{-1}(0)]\text{ is acyclic} \qquad\text{and}\qquad D[c^{-1}(1)]\text{ is acyclic}.

The color classes need not be independent, and either class may be empty. Directed triangles are allowed in the input.

Preamble

import Definitions.Def_opg169_planar_dichromatic

Formal statement

namespace OPG169

universe u

/-- OPG-169: every orientation of a finite simple planar graph admits a
vertex two-coloring whose two induced color classes are acyclic. -/
theorem root_problem
    {V : Type u} [Fintype V] (G : SimpleGraph V) (D : Digraph V)
    (hplanar : IsPlanar G) (horientation : IsOrientationOf D G) :
    HasAcyclicTwoColoring D := by sorry

end OPG169

Source

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

Read-back

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

Let $V$ be a type in a fixed universe with a finite-type structure, let $G$ be a simple graph on $V$ , and let $D$ be a binary relation on $V$ . Assume that there is an injective map $p:V\to\mathbb R^2$ such that no vertex other than the endpoints of an edge lies on that edge’s closed straight segment, and such that the closed segments for any two edges with pairwise distinct endpoints are disjoint. Assume also that $D$ has no loops, every directed arc of $D$ joins adjacent vertices of $G$ , and for every edge with endpoints $u,v$ , exactly one of $D(u,v)$ and $D(v,u)$ holds. Then there exists a coloring $c:V\to\mathrm{Fin}\,2$ such that, for each of the two colors $k$ , there is no list $vs=x$ followed by a middle list and then $y$ having length at least $3$ , no repeated vertices, directed arcs between every consecutive pair, and an arc from $y$ back to $x$ , all of whose vertices satisfy $c(v)=k$ .

Human review

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

View graph