Skip to content

Erdős problem 753

The list chromatic number χL(G)\chi_L(G) is defined to be the minimal kk such that for any assignment of a list of kk colours to each vertex of GG (perhaps different lists for different vertices) a colouring of each vertex by a colour on its list can be chosen such that adjacent vertices receive distinct colours.

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

753.lean

Retained formal statement1 of 2

The list chromatic number χL(G)\chi_L(G) is defined to be the minimal kk such that for any assignment of a list of kk colours to each vertex of GG (perhaps different lists for different vertices) a colouring of each vertex by a colour on its list can be chosen such that adjacent vertices receive distinct colours.

Does there exist some constant c>0c>0 such that χL(G)+χL(Gc)>n1/2+c\chi_L(G)+\chi_L(G^c)> n^{1/2+c} for every graph GG on nn vertices (where GcG^c is the complement of GG)?

A problem of Erdős, Rubin, and Taylor.

The answer is no: Alon [Al92] proved that, for every nn, there exists a graph GG on nn vertices such that χL(G)+χL(Gc)≪(nlog⁡n)1/2,\chi_L(G)+\chi_L(G^c)\ll (n\log n)^{1/2}, where the implied constant is absolute.

FormalConjectures/ErdosProblems/753.leanErdos753.erdos_7537 linesExact file
False ↔  ∃ c,    0 < c ∧      ∀ (n : ℕ),        0 < n →          ∀ (G : SimpleGraph (Fin n)),            ↑n ^ (1 / 2 + c) < ↑(Erdos753.listChromaticNumber G) + ↑(Erdos753.listChromaticNumber Gᶜ)
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.