Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Sands-Sauer-Woodrow Corollary 2: a two-coloured tournament has a monochromatic sink

Open
SandsSauerWoodrow.two_coloured_tournament_sink

by marwahaha · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsgraph-theory

This is Corollary 2 of Sands, Sauer and Woodrow, On monochromatic paths in edge-coloured digraphs, J. Combin. Theory Ser. B 33 (1982), 271–275, stated on p. 273.

Let TTT be a tournament on a nonempty finite set VVV of vertices — that is, a directed graph in which every two distinct vertices are joined by exactly one arc — and let each arc of TTT carry one of three colours, only the colours 000 and 111 being used. Then there is a vertex vvv such that for every vertex x≠vx \neq vx=v there is a directed path from xxx to vvv all of whose arcs have the same colour.

The common colour may depend on xxx, and the path is not required to be short: the source observes that no bound on its length is possible. In the source's terms the conclusion says that the tournament contains a monochromatic sink. This is the settled two-colour case of the question raised by Erdős on p. 275 of the same paper, whether three colours force either a rainbow directed triangle or such a vertex; that three-colour question is open.

Formalization Note. A colouring is a function on all ordered pairs of vertices; the hypothesis constrains its values only on arcs, which is all the conclusion depends on. The source allows loops and multiple edges; here a digraph is a relation and TTT is a tournament, so neither occurs. Nonemptiness of VVV is required: for an empty vertex set there is no vertex vvv to exhibit.

Preamble
import Definitions.Def_opg1808_colored_tournaments

open OPG1808

universe u
Formal statement
namespace SandsSauerWoodrow

theorem two_coloured_tournament_sink {V : Type u} [Fintype V] [Nonempty V]
    (D : Digraph V) (color : ArcColoring V) (htournament : IsTournament D)
    (htwo : ∀ u v, D u v → (color u v = 0 ∨ color u v = 1)) :
    ∃ v : V, ∀ x : V, x ≠ v → MonochromaticallyReaches D color x v := by sorry

end SandsSauerWoodrow
Source
B. Sands, N. Sauer, R. Woodrow, On monochromatic paths in edge-coloured digraphs, J. Combin. Theory Ser. B 33 (1982), no. 3, 271-275. Theorem 1 (pp. 271-273); Corollary 2 (p. 273); Theorem 3 (pp. 274-275); PROBLEM (p. 275).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me