Erdős problem 753
The list chromatic number is defined to be the minimal such that for any assignment of a list of colours to each vertex of (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
FormalConjectures/ErdosProblems/
753.lean
Retained formal statement
Alon [Al92] proved that, for every , there exists a graph on vertices such that where the implied constant is absolute.
∃ C, 0 < C ∧ ∀ (n : ℕ), 2 ≤ n → ∃ G, ↑(Erdos753.listChromaticNumber G) + ↑(Erdos753.listChromaticNumber Gᶜ) ≤ C * (↑n * Real.log ↑n) ^ (1 / 2)SolvedStatement only, no proof