Erdős Problem #1174

The question

erdos_1174.parts.i. Erdős Problem 1174, part (i) [Va99, 7.91]. A problem of Erdős and Hajnal: does there exist a graph $G$ with no $K_4$ such that every edge colouring of $G$ with countably many colours contains a monochromatic $K_3$?

For simplicity the colourings are given on all unordered pairs ${\mathrm{Sym}}_2(V)$; only the values on the edges of $G$ matter, since a monochromatic triangle is witnessed by edges alone.

Shelah proved that a graph with this property can consistently exist, so the problem is not disprovable in ZFC; whether such a graph exists outright remains open.

erdos_1174.parts.ii. Erdős Problem 1174, part (ii) [Va99, 7.91]. A problem of Erdős and Hajnal: does there exist a graph $G$ with no $K_{{\aleph }_1}$ (that is, every clique of $G$ is countable) such that every edge colouring of $G$ with countably many colours contains a monochromatic $K_{{\aleph }_0}$ (an infinite clique all of whose edges receive the same colour)?

For simplicity the colourings are given on all unordered pairs ${\mathrm{Sym}}_2(V)$; only the values on the edges of $G$ matter.

Shelah proved that a graph with this property can consistently exist, so the problem is not disprovable in ZFC; whether such a graph exists outright remains open.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.ErdosProblems.«1174» (2 statements).

theorem erdos_1174.parts.i :
    ∃ (V : Type) (G : SimpleGraph V), G.CliqueFree 4 ∧
      ∀ c : Sym2 V → ℕ, ∃ x y z : V,
        G.Adj x y ∧ G.Adj y z ∧ G.Adj x z ∧
        c s(x, y) = c s(y, z) ∧ c s(y, z) = c s(x, z)

theorem erdos_1174.parts.ii :
    ∃ (V : Type) (G : SimpleGraph V),
      (∀ S : Set V, G.IsClique S → #S ≤ ℵ₀) ∧
      ∀ c : Sym2 V → ℕ, ∃ S : Set V, G.IsClique S ∧ S.Infinite ∧
        ∃ k : ℕ, ∀ x ∈ S, ∀ y ∈ S, x ≠ y → c s(x, y) = k

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already — check erdosproblems.com/1174. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• erdosproblems.com/1174
• [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999), problem 7.91.

Source and licence

Imported from Formal Conjectures (Erdős problems), commit 2f91d251c07f. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.