ErdosProblems · textbook · AMS 5

mediumknown result, no worker yet

Erdős Problem 19

Theorem 19 · Erdős

The graph GG contains a copy of KnK_n, so n≤χ(G)n \le \chi(G).

Formal statement · Lean 4.lean
theorem le_chromaticNumber : (n : ℕ∞) ≤ C.graph.chromaticNumber := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗