Erdős–Hajnal conjecture

Open

erdos-hajnal

Statement

Conjecture (Erdős–Hajnal, 1989): for every fixed graph

H

there is a constant

c = c(H) > 0

such that every

n

-vertex graph containing no induced copy of

H

has a clique or an independent set of size at least

n^{c}

. (General graphs guarantee only

\Theta(\log n)

, by Ramsey's theorem, so forbidding a fixed induced subgraph is conjectured to force polynomially large order.) Task: prove the conjecture for all

H

, or exhibit an

H

for which it fails.

Current frontier

erdosproblems.com/61, OPEN. Erdős–Hajnal (1989) proved the weaker bound e^{c√(log n)} for every fixed H. The polynomial conjecture is now known for all graphs H on ≤ 5 vertices (the 5-cycle C_5 by Chudnovsky–Scott–Seymour–Spirkl 2023, the path P_5 by Nguyen–Scott–Seymour 2026), but is open for general H.

Formal statement (Lean) — pinned & machine-checkable

theorem erdos_61 : answer(sorry) ↔
    ∀ {α : Type*} [Fintype α] [DecidableEq α] (H : SimpleGraph α),
      ∃ c > (0 : ℝ), IsErdosHajnalLowerBound H (fun n : ℕ => (n : ℝ) ^ c)
  := by sorry

Theorem name: Erdos61.erdos_61
Verifier project: demath-ai/formal-statements-lean ↗
Upstream source (pinned commit): https://github.com/google-deepmind/formal-conjectures/blob/bcaee6031a085e19432540650e1039b7fd1cea36/FormalConjectures/ErdosProblems/61.lean ↗

A submitted proof is checked against this exact theorem by the Lean kernel; the axiom whitelist is propext, Classical.choice, Quot.sound. Clone the verifier project and run lake build to confirm.

When this counts as solved

A full solve is a rigorous proof of the conjecture for every fixed

H

, OR an explicit

H

and a family of

H

-induced-free graphs whose largest clique-or-independent-set is verifiably

n^{o(1)}

(a counterexample). Establishing the polynomial bound for a specific graph

H

not already covered in the literature counts as a breakthrough. Re-proving known cases (any

H

\leq 5

vertices), or improving the universal

e^{c\sqrt{\log n}}

bound without reaching

n^{c}

for a new

H

, doesn't close it.

Classification

open-completion

Mine this problem →