Problem 22

Let $\epsilon>0$ and $n$ be sufficiently large depending on $\epsilon$ . Is there a graph on $n$ vertices with $\geq n^2/8$ many edges which contains no $K_4$ such that the largest independent set has size at most $\epsilon n$ ?

Source: erdosproblems.com/22

Graph theory

Wiki page

Status

SolvedProved

An accepted solution exists. The statement is true.

Proved. The site's label reads "PROVED (LEAN)"; its suffix is a catalog label explained under Formalization. The status-defining source is Theorem 1.9 of Fox, Loh and Zhao (Combinatorica 35 (2015), no. 4, 435--476, refereed): there is an absolute constant $c'>0$ such that for each positive integer $n$ there is an $n$ -vertex $K_4$ -free graph with at least $n^2/8$ edges and independence number at most $c'n\,(\log\log n)^{3/2}/(\log n)^{1/2}$ . Since the factor $(\log\log n)^{3/2}/(\log n)^{1/2}$ tends to $0$ , the independence number is at most $\epsilon n$ once $n$ is large in terms of $\epsilon$ , which answers the question with yes for every $\epsilon>0$ . Bollobás and Erdős's own Theorem (1976) gives $f(n,4,l)=(1+o(1))n^2/8$ for $l=o(n)$ , that is, graphs with $(1/8-o(1))n^2$ edges, which is why they left the threshold case as a question. The companion Theorem 1.8 of the same paper shows the independence number cannot be pushed below $cn\log\log n/\log n$ at $n^2/8$ edges, so the construction is within a factor of order $(\log\log n)^{1/2}(\log n)^{1/2}$ of best possible. The claim page is Fox, Loh and Zhao (accepted on the refereed publication and the curator's credit); the 2026 Lean proof in the lean-proofs repository declares itself a formalization of their theorem and is recorded on that page as a formalization link; it gives no formalized evidence.

FLZ15: Fox, J., Loh, P.-S. and Zhao, Y., The critical window for the classical Ramsey-Turán problem. Combinatorica 35 (2015), no. 4, 435--476, doi:10.1007/s00493-014-3025-3 (published online 22 October 2014, per the Crossref record and the arXiv listing's journal reference); arXiv:1208.3276v3 (23 September 2014), the version cited; the journal text is not held. Theorem 1.1 (Szemerédi's theorem, quoted) and Problems 1.2--1.3, p. 2; Theorems 1.5--1.6, p. 3; Theorems 1.7--1.10, p. 4; Theorem 1.11, p. 5. Library home: Fox, Loh and Zhao 2015.
BoEr76: Bollobás, B. and Erdős, P., On a Ramsey-Turán type problem. J. Combinatorial Theory Ser. B 21 (1976), no. 2, 166--168, doi:10.1016/0095-8956(76)90057-5 (received March 11, 1975). The Theorem, p. 166; the closing questions, p. 168. Library home: Bollobás and Erdős 1976 (a Rényi archive scan).
Sz72: Szemerédi, E., Graphs without complete quadrilaterals (in Hungarian). Mat. Lapok 23 (1972), 113--116 (so dated in the formal-conjectures file; the reference lists of [BoEr76] and of the 1983 Erdős--Hajnal--Sós--Szemerédi paper print 1973). Not held; its theorem is quoted as Theorem 1.1 of [FLZ15] (p. 2) and as display (1) of [BoEr76] (p. 166).
Er90: Erdős, Paul, Some of my favourite unsolved problems. A tribute to Paul Erdős (1990), 467--478. Site source key; not held (after the Rényi archive's 1989 cutoff). [FLZ15] (p. 2) records that the question "was later featured in the Erdős paper [12] from 1990 entitled 'Some of my favourite unsolved problems'".
Cs25: Csaba, B., On the Ramsey-Turán problem for 4-cliques. arXiv:2503.00644v1 (1 March 2025), 12 pp.; SIAM J. Discrete Math. 39 (2025), no. 2, 1201--1212, doi:10.1137/23M1619794 (Crossref record read; the journal text is not held). Theorem 1.3, p. 2 of the preprint. Context on the critical window; the preprint is filed as Csaba 2025.

Problem 22

Status

Proof claims

Discussion