Erdős problem 596
Erdős Problem 596 (Erdős–Hajnal, [Er87]). For which graph pairs is it true that
Sources
FormalConjectures/ErdosProblems/
596.lean
Retained formal statement
Erdős Problem 596 (Erdős–Hajnal, [Er87]). For which graph pairs is it true that
(1) for every there is a graph without a such that any -colouring of 's edges contains a monochromatic , and yet (2) for every graph without a there is an -colouring of 's edges with no monochromatic ?
Erdős and Hajnal originally conjectured that no such pair exists; but witnesses it (Nešetřil–Rödl + Erdős–Hajnal). The full question is to characterise the class of all such pairs, recorded here as answer(sorry).
See Problem 595 for the specific case .
∀ {U₁ U₂ : Type} (G₁ : SimpleGraph U₁) (G₂ : SimpleGraph U₂), G₁.IsErdosHajnalExceptional G₂ ↔ (fun {U₁ U₂} => sorry) G₁ G₂OpenStatement only, no proof