Erdős–Hajnal conjecture for all paths

Open

TenChallenges.challenge_05

by utkuokur · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

erdos-hajnalgraph-theorypathsten-challenges

The Erdős–Hajnal conjecture for all paths. For every $r\in\mathbb N$ there is a constant $c_r>0$ such that every finite graph with no induced path on $r$ vertices has a clique or an independent set of size at least $n^{c_r}$ , where $n$ is its number of vertices:

\forall r\ \ \exists c_r>0\ \ \forall G\ P_r\text{-free}:\quad \max(\omega(G),\alpha(G))\ \ge\ n^{c_r}.

Known for $r\le 5$ ; open for $r\ge 6$ .

Formalization Note. The statement is ∀ r, statement_05 r, where statement_05 r is the Erdős–Hajnal property for pathGraph r.

Preamble

import Definitions.Def_TenChallenges_Challenge_05

Formal statement

namespace TenChallenges
theorem challenge_05 : ∀ r : ℕ, statement_05 r := by sorry
end TenChallenges

Source

P. Erdős, A. Hajnal, Ramsey-type theorems, Discrete Appl. Math. 25 (1989), https://doi.org/10.1016/0166-218X(89)90045-0 (the conjecture, restricted to paths); V. Bajpai, N. Bowler, J. Carmesin, U. Okur, 10 Scalable Challenges in Combinatorics, AI4Math @ CICM 2026, challenge 5 (full form)

Read-back

What the Lean code literally says, in plain math · claude-fable-5-1

Read-back of the theorem TenChallenges.challenge_05.

The statement is

\forall\, r \in \mathbb{N},\quad \mathrm{statement\_05}(r),

where $\mathbb{N} = \{0, 1, 2, \dots\}$ (so $r = 0$ , $r = 1$ and $r = 2$ are included), and $\mathrm{statement\_05}(r)$ is $\mathrm{ErdosHajnalConjectureFor}(P_r)$ for the path graph $P_r$ . Unfolding both definitions, the theorem asserts, for every natural number $r$ :

\exists\, c \in \mathbb{R}:\; 0 < c \;\wedge\; \forall\, V\ \text{finite},\ \forall\, G \text{ a simple graph on } V:\quad P_r \not\trianglelefteq G \;\Longrightarrow\; \exists\, s \subseteq V:\ \big(s \text{ is a clique of } G \;\vee\; s \text{ is a clique of } \overline{G}\big) \;\wedge\; |s| \ge |V|^{c}.

Meaning of each piece:

$P_r$ : Mathlib's path graph on $r$ vertices; vertex set $\{0, 1, \dots, r-1\}$ , with $i$ adjacent to $j$ exactly when $i + 1 = j$ or $j + 1 = i$ (the Hasse diagram of the linear order on $\{0,\dots,r-1\}$ ). It has $r$ vertices and $r-1$ edges for $r \ge 1$ ; $P_0$ has no vertices, $P_1$ is an isolated vertex, $P_2$ is a single edge.
$c$ : a real number with $0 < c$ (strict; no upper bound). It is chosen after $r$ and before $V$ and $G$ , so it may depend on $r$ but must be uniform over all finite graphs $G$ for that $r$ .
$V$ : ranges over all types in the lowest universe (ordinary sets) equipped with a finiteness structure, i.e. all finite vertex sets, including the empty set.
$G$ : ranges over all simple graphs on $V$ (irreflexive, symmetric adjacency $\sim_G$ ).
Hypothesis $P_r \not\trianglelefteq G$ : there is no graph embedding of $P_r$ into $G$ ; a graph embedding is an injective map $f : \{0,\dots,r-1\} \to V$ such that $f(i) \sim_G f(j)$ if and only if $|i - j| = 1$ for all $i, j$ . Equivalently, $G$ has no induced subgraph isomorphic to $P_r$ : there are no $r$ distinct vertices $v_0, \dots, v_{r-1}$ with $v_i \sim_G v_{i+1}$ for $0 \le i \le r-2$ and $v_i \not\sim_G v_j$ for $|i-j| \ge 2$ . Paths on $r$ vertices with chords are not excluded; only chordless (induced) ones are.
Conclusion: there is a finite set $s$ of vertices of $G$ (possibly empty) such that either $s$ is a clique of $G$ (for all $u \ne v$ in $s$ , $u \sim_G v$ ) or $s$ is a clique of the complement $\overline{G}$ (adjacency " $u \ne v$ and $u \not\sim_G v$ "), i.e. an independent set of $G$ (for all $u \ne v$ in $s$ , $u \not\sim_G v$ ); and, as real numbers, $|s| \ge |V|^{c}$ (non-strict), where $|s|$ and $|V|$ are the numbers of elements of $s$ and of $V$ , and $x^{c}$ is the real power with real exponent ( $e^{c \ln x}$ for $x > 0$ , and $0^{c} = 0$ because $c > 0$ ).

Edge cases included by the quantifiers:

$r = 0$ : $P_0$ (no vertices) embeds into every $G$ via the empty map, so the hypothesis is never satisfied and the inner universal statement is vacuous; the claim for $r = 0$ reduces to "there exists a real $c > 0$ ".
$r = 1$ : $P_1$ embeds into $G$ whenever $V \ne \varnothing$ ; the hypothesis therefore holds only for the empty graph on no vertices, where $s = \varnothing$ satisfies $0 \ge 0^{c} = 0$ .
$r = 2$ : the hypothesis says $G$ has no edges; $s = V$ is then an independent set with $|V| \ge |V|^{c}$ required.
For every $r$ : $V = \varnothing$ is allowed (then $|V|^{c} = 0$ and $s = \varnothing$ suffices); $\varnothing$ and every singleton are vacuously both a clique and an independent set, so the conclusion is trivially met whenever $|V|^{c} \le 1$ .

The declaration is stated with a placeholder proof (sorry); the code supplies no proof of the statement.

Human review

Endorsed by Shuze Chen · Nov 4, 2026
Confirmed by the moderator at approval.
Endorsed by utkuokur · Nov 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph