The board / graph theory / #582
Erdős Problem #582
PROVED LEANdatabase updated 2026-02-05
The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
A graph `G` is *edge-Ramsey for triangles* (in arrow notation, \(G \to (K_3, K_3)^e\)) if any \(2\)-colouring of the edges of `G` produces a monochromatic \(K_3\): three pairwise adjacent vertices whose three connecting edges all receive the same colour.
Does there exist a graph \(G\) which contains no \(K_4\), and yet any \(2\)-colouring of the edges produces a monochromatic \(K_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 \(N\) of such a graph are \(21 \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].
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/582.Prize$100
Topicsgraph theory, ramsey theory
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/582
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.