Erdős problem 61
The Erdős–Hajnal Conjecture states that there is a constant for each such that we can take in the above formulation.
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/61.leansorry ↔ ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (H : SimpleGraph α), ∃ c > 0, Erdos61.IsErdosHajnalLowerBound H fun n => ↑n ^ cOpenStatement only, no proof