Skip to content

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

Sources

The source's own material, retained exactly.

9 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

596.lean

Retained formal statement3 of 9

Nešetřil–Rödl [NeRo75]: for every n≥1n \geq 1 there is a C4C_4-free graph whose edges cannot be nn-coloured without a monochromatic C6C_6.

FormalConjectures/ErdosProblems/596.leanErdos596.erdos_596.variants.C4_C6_finite_ramsey1 lineExact file
(SimpleGraph.cycleGraph 4).HasFiniteRamseyProperty (SimpleGraph.cycleGraph 6)
SolvedStatement only, no proof