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
Nguyen, Scott, and Seymour [NSS23] proved the conjecture for , the path on five vertices: every -free graph on 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
∃ c > 0, Erdos61.IsErdosHajnalLowerBound (SimpleGraph.pathGraph 5) fun n => ↑n ^ cSolvedStatement only, no proof