The three-colored tournament problem through order eleven

Open

OPG1808.order_eleven

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

combinatoricsdirected-graphsgraph-theoryopen-problemtournaments

Let $T$ be a nonempty tournament on at most eleven vertices with its arcs colored by three colors. If $T$ has no rainbow directed triangle, then some vertex reaches every target along a monochromatic directed path:

1\le |V(T)|\le11\ \land\ \text{no rainbow directed triangle} \quad\Longrightarrow\quad \exists s\ \forall t,\ s\leadsto t\text{ monochromatically}.

The path color may depend on $t$ . This finite theorem is an open formal target; the cited repository replay is candidate_only, not a proof on the platform.

Preamble

import Definitions.Def_opg1808_colored_tournaments

Formal statement

namespace OPG1808

universe u

/-- The finite root case through eleven vertices. -/
theorem order_eleven
    {V : Type u} [Fintype V] [Nonempty V]
    (D : Digraph V) (color : ArcColoring V)
    (htournament : IsTournament D)
    (horder : Fintype.card V ≤ 11)
    (hnoRainbow : ¬ HasRainbowDirectedTriangle D color) :
    ∃ s : V, IsMonochromaticSource D color s := by sorry

end OPG1808

Source

VibeMathing candidate_only exact-closure replay at commit aa702573cf51c587cccc6d31c28a54bcc64eb5d9, research/artifacts/candidates/opg1808-r05-replay-20260907/README.md; minimum-counterexample reduction: Georgakopoulos--Sprüssel, arXiv:0904.1967v2, pp. 2-3

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. Also assume that the number of vertices satisfies $|V|\le 11$ , and that there do not exist pairwise distinct vertices $a,b,c$ with directed arcs $a\to b$ , $b\to c$ , and $c\to a$ whose three arc colors $\mathrm{color}(a,b)$ , $\mathrm{color}(b,c)$ , and $\mathrm{color}(c,a)$ are pairwise distinct. Then there exists a vertex $s\in V$ such that, for every $t\in V$ , there is a color $k\in\mathrm{Fin}(3)$ and a directed path from $s$ to $t$ of zero or more steps, all of whose arcs have color $k$ ; the color may 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