Erdős problem 944
Let and . Must there exist a graph with chromatic number such that every vertex is critical, yet every critical set of edges has size ?
Sources
FormalConjectures/ErdosProblems/
944.lean
Retained formal statement
Let . Must there exist a graph with chromatic number such that every vertex is critical, yet every critical set of edges has size ?
This was conjectured by Dirac in 1970.
True ↔ ∀ k ≥ 4, ∃ V G, Erdos944.SimpleGraph.IsErdos944 G k 1OpenStatement only, no proof