Skip to content

Erdős problem 61

The Erdős–Hajnal Conjecture states that there is a constant c(H)>0c(H) > 0 for each HH such that we can take f(n)=nc(H)f(n) = n^{c(H)} in the above formulation.

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

61.lean

Retained formal statement4 of 5

Erdős and Hajnal [ErHa89] proved that we can take f(n)=exp(cHlogn)f(n) = \exp(c_H \sqrt{\log n}) for some constant cH>0c_H > 0 depending on HH.

[ErHa89] Erdős, P. and Hajnal, A., Ramsey-type theorems. Discrete Appl. Math. (1989), 37-52.

FormalConjectures/ErdosProblems/61.leanErdos61.erdos_61.variants.erha892 linesExact file
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (H : SimpleGraph α),c > 0, Erdos61.IsErdosHajnalLowerBound H fun n => Real.exp (c * √(Real.logn))
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page