Skip to content

Erdős problem 108

Start work

For every r ≥ 4 and k ≥ 2 is there some finite f(k,r) such that every graph of chromatic number ≥ f(k,r) contains a subgraph of girth ≥ r and chromatic number ≥ k?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

108.lean

Retained formal statement1 of 1

For every r ≥ 4 and k ≥ 2 is there some finite f(k,r) such that every graph of chromatic number ≥ f(k,r) contains a subgraph of girth ≥ r and chromatic number ≥ k?

FormalConjectures/ErdosProblems/108.leanErdos108.erdos_1086 linesExact file
True ↔  ∀ r ≥ 4,    ∀ k ≥ 2,      ∃ f,        ∀ (V : Type u) (G : SimpleGraph V),          Nonempty V → ↑f ≤ G.chromaticNumber → ∃ H, H.coe.girth ≥ r ∧ H.coe.chromaticNumber ≥ ↑k
OpenStatement only, no proof