OPG-1808: rainbow directed triangle or monochromatic source

Open

OPG1808.root_problem

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

combinatoricsdirected-graphsgraph-theoryopen-problemtournaments

Every nonempty finite tournament whose arcs have three colors has one of the following outcomes:

a cyclically oriented triangle whose three arcs have pairwise distinct colors; or
a vertex $s$ such that every vertex $t$ is reachable from $s$ by a directed path of one color.

The color in the second outcome may be selected separately for each target. Rainbow transitive triples are not included in the first outcome.

Preamble

import Definitions.Def_opg1808_colored_tournaments

Formal statement

namespace OPG1808

universe u

/-- OPG-1808 for nonempty finite tournaments: either there is a rainbow
directed triangle or a monochromatic source. -/
theorem root_problem
    {V : Type u} [Fintype V] [Nonempty V]
    (D : Digraph V) (color : ArcColoring V)
    (htournament : IsTournament D) :
    HasRainbowDirectedTriangle D color ∨
      ∃ s : V, IsMonochromaticSource D color s := by sorry

end OPG1808

Source

Open Problem Garden, Monochromatic reachability versus rainbow triangles, https://www.openproblemgarden.org/op/monochromatic_reachability_vs_rainbow_triangles; attributed there to Sands--Sauer--Woodrow, JCTB 33 (1982), 271-275

Read-back

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

Let $V$ be a finite, nonempty type, let $D$ be a binary relation on $V$ , and let $\mathrm{color}$ assign one of three colors to every ordered pair of vertices. Assume that no vertex has a loop, and that for every distinct pair $u,v\in V$ exactly one of $D(u,v)$ and $D(v,u)$ holds. Then either there exist pairwise distinct vertices $a,b,c$ with directed arcs $a\to b$ , $b\to c$ , and $c\to a$ whose three arc colors are pairwise distinct, or there exists a vertex $s\in V$ such that every vertex $t\in V$ can be reached from $s$ by a directed path of zero or more steps whose arcs all share one color in $\mathrm{Fin}(3)$ , with that color allowed to depend on $t$ .

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