Erdős problem 753

The list chromatic number $\chi_L(G)$ is defined to be the minimal $k$ such that for any assignment of a list of $k$ colours to each vertex of $G$ (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

FormalConjectures/ErdosProblems/

753.lean

Retained formal statement2 of 2

Alon [Al92] proved that, for every $n$ , there exists a graph $G$ on $n$ vertices such that $\chi_L(G)+\chi_L(G^c)\ll (n\log n)^{1/2},$ where the implied constant is absolute.

FormalConjectures/ErdosProblems/753.leanErdos753.erdos_753.variants.alon5 linesExact file

1∃ C,2  0 < C ∧3    ∀ (n : ℕ),4      2 ≤ n →5        ∃ G, ↑(Erdos753.listChromaticNumber G) + ↑(Erdos753.listChromaticNumber Gᶜ) ≤ C * (↑n * Real.log ↑n) ^ (1 / 2)

SolvedStatement only, no proof