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

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

61.lean

Retained formal statement5 of 5

Nguyen, Scott, and Seymour [NSS23] proved the conjecture for H=P5H = P_5, the path on five vertices: every P5P_5-free graph on nn vertices has a clique or independent set of polynomial size.

[NSS23] Nguyen, T., Scott, A. and Seymour, P., Induced subgraph density. VII. The five-vertex path. arXiv:2312.15333

FormalConjectures/ErdosProblems/61.leanErdos61.erdos_61.variants.p51 lineExact file
∃ c > 0, Erdos61.IsErdosHajnalLowerBound (SimpleGraph.pathGraph 5) fun n => ↑n ^ c
SolvedStatement only, no proof