Skip to content

Erdős problem 582

Does there exist a graph GG which contains no K4K_4, and yet any 22-colouring of the edges produces a monochromatic K3K_3?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

582.lean

Retained formal statement1 of 1

Does there exist a graph GG which contains no K4K_4, and yet any 22-colouring of the edges produces a monochromatic K3K_3?

Erdős and Hajnal [ErHa67] first asked for the existence of any such graph. Existence was proved by Folkman [Fo70], but with very poor quantitative bounds. (As a result these quantities are often called Folkman numbers.) The current best bounds on the minimal number of vertices NN of such a graph are 21≤N≤78621 \leq N \leq 786, where the lower bound is due to Bikov and Nenov [BiNe20] and the upper bound is due to Lange, Radziszowski, and Xu [LRX14].

FormalConjectures/ErdosProblems/582.leanErdos582.erdos_5821 lineExact file
True ↔ ∃ V x G, G.CliqueFree 4 ∧ Erdos582.EdgeRamseyTriangle G
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.