All open problems
Source labels openChecked July 26, 2026

Erdős ProblemsCombinatorics

Erdős Problem 596

Erdős Problem 596* (Erdős–Hajnal, [Er87]). For which graph pairs (G1,G2)(G_1, G_2) is it true that

Mathematical statement

Erdős Problem 596* (Erdős–Hajnal, [Er87]). For which graph pairs (G1,G2)(G_1, G_2) is it true that

(1) for every n1n \geq 1 there is a graph HH without a G1G_1 such that any nn-colouring of HH's edges contains a monochromatic G2G_2, and yet (2) for every graph HH without a G1G_1 there is an 0\aleph_0-colouring of HH's edges with no monochromatic G2G_2?

Erdős and Hajnal originally conjectured that no such pair exists; but (C4,C6)(C_4, C_6) 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 (G1,G2)=(K4,K3)(G_1, G_2) = (K_4, K_3).

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

erdos_596

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem erdos_596 :     {U₁ U₂ : Type} (G₁ : SimpleGraph U₁) (G₂ : SimpleGraph U₂),      IsErdosHajnalExceptional G₁ G₂       (answer(sorry) :  {U₁ U₂ : Type}, SimpleGraph U₁  SimpleGraph U₂  Prop) G₁ G₂ := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References