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.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/753.lean

Formal Conjectures

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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:753
  • PLBY Lean proofsErdosProblems.Erdos753

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page