Skip to content

Erdős problem 61

Start work

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

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

61.lean

Retained formal statement1 of 5

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.

FormalConjectures/ErdosProblems/61.leanErdos61.erdos_613 linesExact file
sorry ↔  ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (H : SimpleGraph α),    ∃ c > 0, Erdos61.IsErdosHajnalLowerBound H fun n => ↑n ^ c
OpenStatement only, no proof