Does large chromatic number force a subgraph of girth $\ge r$ and chromatic number $\ge k$? (Erdős #108)
Statement
For every $r\geq 4$ and $k\geq 2$, is there some finite $f(k,r)$ such that every graph of chromatic number $\geq f(k,r)$ contains a subgraph of girth $\geq r$ and chromatic number $\geq k$? (The girth of a graph is the length of its shortest cycle; a subgraph of girth $\geq r$ contains no cycle of length $<r$.)
Acceptance. FULLY RESOLVES: a complete proof (machine-checkable Lean/Coq preferred, else a full written proof with all steps) that $f(k,r)$ is finite for all $r\geq 4$ and $k\geq 2$ — or a disproof exhibiting, for some fixed $r\geq 5$ and $k$, graphs of arbitrarily large chromatic number in which every subgraph of girth $\geq r$ has chromatic number $<k$, with proof. No finite computation can close this (classified OPEN on the source site). ADVANCES: a proof of the first open girth case $r=5$ (subgraphs with no triangles or 4-cycles), for all $k$ or even for a single new value of $k$ beyond what is trivial; explicit quantitative upper bounds on $f(k,4)$ extracted from or improving Rödl's argument, with proof; a proof or disproof of the growth question $\lim_k f(k,r+1)/f(k,r)=\infty$; progress on the infinite version (Erdős #740); or exact small values (e.g. the least chromatic number forcing a girth-$\ge 5$ subgraph of chromatic number $\ge 4$) established by exhaustive search with SAT certificates and a finiteness argument for the search space. Deliver the proof file, or the code plus machine-verifiable certificates for any exact-value claims.
Background
Conjectured by Erdős and Hajnal; raised by Erdős repeatedly ([Er71], [Er79b], [Er81], [Er90], [Er95d], and as Problem 3.59 in [Va99]); listed as open on erdosproblems.com/108 (fetched 2026-07-13, status 'open', tagged 'graph theory | chromatic number | cycles'). It is a structural strengthening of Erdős's celebrated 1959 theorem that graphs of arbitrarily large girth and chromatic number exist: here one asks whether high chromatic number alone always CONTAINS such high-girth, high-chromatic structure. Known frontier: Rödl [Ro77] proved the $r=4$ case — every graph of sufficiently large chromatic number contains a triangle-free subgraph of chromatic number $\geq k$ (see Erdős #923, erdosproblems.com/923). Every case $r\geq 5$ is open. The infinite version — whether every graph of infinite chromatic number contains a subgraph of infinite chromatic number and girth $>k$ — is also open (see Erdős #740, erdosproblems.com/740). In [Er79b] Erdős further asks whether $\lim_{k\to\infty}f(k,r+1)/f(k,r)=\infty$. A formalized Lean statement exists in Google DeepMind's formal-conjectures repository, and the problem appears in the UCSD Erdős graph-problem collection. The attacker's tools: this is proof-shaped extremal graph theory — the target is a Rödl-style argument surviving the exclusion of $4$-cycles; side channels include quantitative bounds extracted from Rödl's proof for $f(k,4)$, SAT/CP experiments on small graphs to estimate $f(3,5)$-type values, and Lean formalization of Rödl's theorem.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #108 (T. F. Bloom) | website |
| REF-02 | Formalized statement of Erdős #108 (Lean, formal-conjectures) | website |
| REF-03 | Subgraphs of large girth — entry in the Erdős graph problem collection (UCSD) | website |
| REF-04 | Erdős Problem #740 (the infinitary version) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.