Skip to content

Erdős problem 923

Start work

Is it true that, for every kk, there is some f(k)f(k) such that if GG has chromatic number ≥f(k)\geq f(k) then GG contains a triangle-free subgraph with chromatic number ≥k\geq k?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/923.lean

Formal Conjectures

FormalConjectures/ErdosProblems/923.leanErdos923.erdos_9233 linesExact file
True ↔  ∀ (V : Type u_1) (n : ℕ),    ∃ k, ∀ (G : SimpleGraph V), ↑k ≤ G.chromaticNumber → ∃ H ≤ G, ↑n ≤ H.chromaticNumber ∧ H.CliqueFree 3
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:923
  • PLBY Lean proofsErdosProblems.Erdos923

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry