Motivation

Ramsey's theorem guarantees that every graph on $n$ vertices has a clique or an independent set of size about $\tfrac12\log_2 n$, and random graphs show that this is best possible. The Erdős–Hajnal conjecture says that forbidding any single induced subgraph $H$ changes the picture completely: $H$-free graphs should contain cliques or independent sets of polynomial size $n^{c_H}$. The conjecture is a central problem of structural graph theory, linking induced subgraphs, perfect graphs and Ramsey theory (Chudnovsky 2014).

Timeline.

• 1977/1989 — Erdős and Hajnal pose the conjecture and prove that $H$-free graphs contain cliques or independent sets of size $\exp(c\sqrt{\log n})$ (Erdős–Hajnal 1989).
• 2001 — Alon, Pach and Solymosi show that the conjecture is closed under substitution, giving it for a family of graphs built from small cases (Alon–Pach–Solymosi 2001).
• 2008 — Chudnovsky and Safra prove it for the bull (Chudnovsky–Safra 2008).
• 2023 — Chudnovsky, Scott, Seymour and Spirkl prove it for the five-vertex cycle (Chudnovsky–Scott–Seymour–Spirkl 2023).
• 2023 — Bucić, Nguyen, Scott and Seymour improve the general bound to $\exp(c\sqrt{\log n\log\log n})$ (Bucić–Nguyen–Scott–Seymour 2023).
• 2023/2026 — Nguyen, Scott and Seymour prove it for the five-vertex path $P_5$, completing all graphs on five vertices; they also show that for every path $P$ and every $d<1$, $P$-free graphs contain cliques or independent sets of size $2^{(\log n)^d}$ (Nguyen–Scott–Seymour, ISD V, ISD VII).

The conjecture is open for the six-vertex path $P_6$, and for every longer path.

Setting

All graphs are finite and simple. A set of vertices is a clique if its vertices are pairwise adjacent and an independent set (or stable set) if they are pairwise non-adjacent. For graphs $G$ and $H$, $G$ is $H$-free if no induced subgraph of $G$ is isomorphic to $H$. The path $P_r$ has $r$ vertices $v_1,\dots,v_r$ and edges $v_iv_{i+1}$. For $r\in\mathbb N$ let $\mathrm{EH}(r)$ be the statement

$$\exists\, c>0\ \ \forall G\ P_r\text{-free}:\quad G \text{ has a clique or an independent set of size at least } |V(G)|^{c}.$$

The constant $c$ may depend on $r$ but not on $G$.

Formalization targets

Goal

$$\forall r\in\mathbb N:\quad \mathrm{EH}(r).$$

Rungs

$\mathrm{EH}(4)$ ($P_4$-free graphs are cographs, hence perfect, and $c=\tfrac12$ works), $\mathrm{EH}(5)$ (Nguyen, Scott, Seymour), and the first open rung $\mathrm{EH}(6)$. The rungs $r\le 3$ are exercises: $P_2$-free graphs are edgeless, $P_3$-free graphs are disjoint unions of cliques.

Significance

Paths are the test case for the conjecture: a proof for all paths would, by the substitution theorem and the known closure properties, settle it for a large class of graphs, and the methods developed for $P_5$ (sparse–dense dichotomies, "polynomial Rödl" theorems) are the current state of the art. The weaker near-polynomial bound $2^{(\log n)^{1-o(1)}}$ is known for all paths, so the gap to be closed is precisely the exponent.

Formalizing the rungs builds the induced-subgraph vocabulary (induced embeddings of paths, cographs, the clique–independent set dichotomy) on top of Mathlib's SimpleGraph. $\mathrm{EH}(4)$ via perfection of cographs is a realistic first project; $\mathrm{EH}(5)$ is a long paper with no machine-checked proof. The goal and $\mathrm{EH}(6)$ are open.

Difficulty

The Erdős–Hajnal argument gives only $\exp(c\sqrt{\log n})$ because each step of its density increment loses a constant factor; the polynomial regime requires structure specific to the forbidden graph. For $P_5$ the proof needs a new "polynomial" version of Rödl's theorem for $P_5$-free graphs together with a delicate analysis of sparse and dense configurations; none of it is known to extend to $P_6$. The naive idea, induction on $r$ by deleting a vertex, loses the forbidden structure.

Formalization scope

Graphs are Mathlib's SimpleGraph V with [Fintype V] and V : Type (the lowest universe); $H$-freeness is ¬ H ⊴ G with Mathlib's induced-subgraph relation ⊴ (an injective graph homomorphism that reflects adjacency). ErdosHajnalConjectureFor H states: there is a real $c>0$ such that every finite $H$-free graph $G$ has a Finset $s$ which is a clique of $G$ or a clique of the complement $G^{c}$, with $|s|\ge |V|^{c}$ as real numbers (real exponentiation). The rung statement_05 r is ErdosHajnalConjectureFor (pathGraph r), with Mathlib's pathGraph r on Fin r. For $r\le 1$ the path embeds in every graph with enough vertices, so the hypothesis is vacuous or nearly so; the content starts at $r=2$. The goal is ∀ r, statement_05 r.

No trivialising reading: $c$ is chosen before $G$, the empty graph on $0$ vertices satisfies the conclusion with $s=\emptyset$ since $0^c=0$, and the clique-or-independent-set alternative is genuine. The Lean definitions are copied verbatim from the Ten Challenges repository. Because the definitions are identical, a proof of the goal or of any rung produced here can also be submitted on the Ten Challenges website, https://tenchallenges.github.io/ten-challenges/, which checks submissions automatically against the same statements and records accepted ones on its public leaderboard; contributors are welcome to do both. Contributions welcome: an API for $P_r$-freeness (characterisations of $P_3$-free and $P_4$-free graphs), perfection of cographs, the exercises $r\le 3$, decompositions of $\mathrm{EH}(4)$ and $\mathrm{EH}(5)$.

Selected references

• Ten Challenges website: problem statements, automatic checker and leaderboard. https://tenchallenges.github.io/ten-challenges/
• V. Bajpai, N. Bowler, J. Carmesin, U. Okur, 10 Scalable Challenges in Combinatorics: A Public Benchmark Formalised in Lean, AI4Math workshop at CICM 2026. https://cicm-conference.org/2026/ai4math/04-okur.pdf — Lean sources: https://github.com/TenChallenges/ten-challenges (challenge 5).
• P. Erdős, A. Hajnal, Ramsey-type theorems, Discrete Appl. Math. 25 (1989), 37–52. https://doi.org/10.1016/0166-218X(89)90045-0
• M. Chudnovsky, The Erdős–Hajnal conjecture: a survey, J. Graph Theory 75 (2014), 178–190. https://doi.org/10.1002/jgt.21730
• N. Alon, J. Pach, J. Solymosi, Ramsey-type theorems with forbidden subgraphs, Combinatorica 21 (2001), 155–170. https://doi.org/10.1007/s004930100016
• M. Chudnovsky, S. Safra, The Erdős–Hajnal conjecture for bull-free graphs, J. Combin. Theory Ser. B 98 (2008), 1301–1310. https://doi.org/10.1016/j.jctb.2008.02.005
• M. Chudnovsky, A. Scott, P. Seymour, S. Spirkl, Erdős–Hajnal for graphs with no 5-hole, Proc. London Math. Soc. 126 (2023), 997–1014. https://doi.org/10.1112/plms.12504
• M. Bucić, T. Nguyen, A. Scott, P. Seymour, Induced subgraph density. I. A loglog step towards Erdős–Hajnal, 2023. https://arxiv.org/abs/2301.10147
• T. Nguyen, A. Scott, P. Seymour, Induced subgraph density. V. All paths approach Erdős–Hajnal, 2023. https://arxiv.org/abs/2307.15032
• T. Nguyen, A. Scott, P. Seymour, Induced subgraph density. VII. The five-vertex path, Proc. London Math. Soc. (2026). https://arxiv.org/abs/2312.15333