Does every graph with chromatic number $ℵ_{1}$ contain an infinitely connected subgraph with chromatic number $ℵ_{1}$ ?

Worked, still open.

graph theory · solved · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

formal

AMS 5 · solved (literature)

theorem erdos_1067 :
    answer(False) ↔ ∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = ℵ_ 1 →
      ∃ (H : G.Subgraph), H.coe.chromaticCardinal = ℵ_ 1 ∧ InfinitelyConnected H.coe

formal-conjectures/1067.lean ↗

status

solved

formal

status

Search Vela