Papers With

← All papers
First page of High-chromatic tournament parts without a complete pair of cyclic triangles

High-chromatic tournament parts without a complete pair of cyclic triangles

Guantao Chen, Hein van der Holst, Shengze Wang

math.CO Oct 27, 2026 · v1
formalization combinatorics
Read PDF arXiv abstract Code
TL;DR
The main theorem was formally verified in Lean 4 using an AI-generated formalization, with the octahedral Tucker lemma and Erdős's high-girth graph existence assumed as axioms.
Abstract
Nguyen, Scott, and Seymour conjectured that any two disjoint subtournaments of sufficiently large chromatic number contain cyclic triangles, one in each subtournament, with all edges between them oriented in the same direction. We disprove this conjecture by constructing, for every positive integer $d$, a tournament $T$ with a vertex partition $(X,Y)$ such that $χ(T[X]),χ(T[Y])\ge d$, but no cyclic triangle in either part is complete to a cyclic triangle in the other. Our construction combines a graph of large girth and large chromatic number with a variant of Kneser graphs defined in terms of binary functions. We give two proofs of the required chromatic lower bound, one using the Borsuk–Ulam theorem and the other using the octahedral form of Tucker's lemma.
Problem

Nguyen, Scott, and Seymour conjectured that any two disjoint subtournaments of large enough chromatic number contain cyclic triangles, one in each part, with all edges between them oriented the same way. The question is whether this conjecture holds.

Approach

For every d, the authors build a tournament with a vertex partition (X,Y) in which both parts have chromatic number at least d. The construction combines a graph of large girth and large chromatic number with a 'binary function graph', a Kneser-like variant defined on {-1,1}-valued functions. The required chromatic lower bound is proved twice, once via the Borsuk–Ulam theorem and once via the octahedral Tucker lemma. The main result was formalized in Lean 4 by AI and checked by Lean, taking Tucker's lemma and Erdős's graph existence theorem as assumptions.

Results

The conjecture is disproved. For every d there is a tournament whose two parts have chromatic number at least d, yet no cyclic triangle in one part is complete to a cyclic triangle in the other.