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.
Sources
FormalConjectures/ErdosProblems/
61.lean
Retained formal statement
Erdős and Hajnal [ErHa89] proved that we can take for some constant depending on .
[ErHa89] Erdős, P. and Hajnal, A., Ramsey-type theorems. Discrete Appl. Math. (1989), 37-52.
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (H : SimpleGraph α), ∃ c > 0, Erdos61.IsErdosHajnalLowerBound H fun n => Real.exp (c * √(Real.log ↑n))SolvedStatement only, no proof