Erdős problem 639
Is it true that if the edges of are 2-coloured then there are at most many edges which do not occur in a monochromatic triangle?
Sources
FormalConjectures/ErdosProblems/
639.lean
Is it true that if the edges of are 2-coloured then there are at most many edges which do not occur in a monochromatic triangle?
Solved by Erdős, Rousseau, and Schelp for large , but unpublished. Alon has observed that this also follows from a result of Pyber [Py86], which states that (for large enough ) at most monochromatic cliques cover all edges of a -coloured .
This problem was solved completely by Keevash and Sudakov [KeSu04], who proved that the correct threshold is for all , is for , and is for .
Since the bound fails for small (at the threshold is ), the statement is formalized in the asymptotic reading in which the problem was posed and solved: for all sufficiently large , every -colouring of the edges of leaves at most edges not occurring in a monochromatic triangle. Edges of are the non-diagonal unordered pairs Sym2 (Fin n); an edge occurs in a monochromatic triangle if and only if there is a third vertex with .
The linked file proves the bound for every finite vertex type with at least vertices, which gives the atTop reading below, and collects the uncovered edges as the edge set of a graph rather than as a set of pairs.
True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : Sym2 (Fin n) → Fin 2), {e | ¬e.IsDiag ∧ ∀ (x y : Fin n), e = s(x, y) → ¬∃ z, z ≠ x ∧ z ≠ y ∧ C s(x, z) = C e ∧ C s(y, z) = C e}.ncard ≤ n ^ 2 / 4