---

Claim. Problem 801 asks whether a graph $G$ on $n$ vertices with no independent set on more than $n^{1/2}$ vertices must have a set of at most $n^{1/2}$ vertices spanning $\gg n^{1/2}\log n$ edges. Alon answers yes. Theorem 1.2 of Independence numbers of locally sparse graphs and a Ramsey type problem states that if the independence number of $G$ is smaller than $\lfloor\sqrt n\rfloor$, then some set of $\lfloor\sqrt n\rfloor$ vertices of $G$ contains at least $\Omega(\sqrt n\log n)$ edges; the abstract gives the conclusion with an absolute constant $c'>0$, as at least $c'\sqrt n\log n$ edges. The paper says the bound is tight and settles Erdős's problem, the tightness being Proposition 3.1: for every $1<m\le n$ there is a graph on $n$ vertices with independence number below $m$ in which every $m$-set spans at most $cm\ln(en/m)$ edges, which at $m=\lfloor\sqrt n\rfloor$ is $O(\sqrt n\log n)$. The proof splits on the average degree: a dense graph has a random $\lfloor\sqrt n\rfloor$-set with the required expected edge count, and in a sparse one either some neighborhood is dense enough or a cleaned random subset is triangle-free, so that the Ajtai--Komlós--Szemerédi bound on its independence number forces the edges. Erdős posed the question in 1979 for $f(n;m)$ at the threshold $m=[n^{1/2}]$, the hypothesis being that every set of $m$ vertices contains an edge, which is Alon's hypothesis $\alpha(G)<m$.

Scope. Full. Alon states the theorem with Erdős's hypothesis $\alpha(G)<\lfloor\sqrt n\rfloor$. The site's wording, no independent set on more than $n^{1/2}$ vertices, also admits graphs with $\alpha(G)=\lfloor\sqrt n\rfloor$, which the theorem as printed does not cover; that boundary case follows from the printed theorem by a twin blow-up recorded in the problem page's Current assessment as an authored reduction, and Alon's p. 7 says that his proof extends to every threshold $n^\epsilon\le m\le n/2$. The Lean development linked above states the result under the site's non-strict hypothesis.

Depends on. Nothing in this wiki.

Acceptance. Reviewed: the site's curator, T. F. Bloom, labels the problem PROVED and credits the proof to this paper in the problem's one-sentence commentary (read 2026-09-18); the site's discussion thread and proof-claim tab are empty. Refereed: the paper appeared in Random Structures Algorithms 9 (1996), no. 3, 271--278 (Crossref record, issue dated October 1996). The pages cited are those of the author's eight-page preprint from his publication list (the preprint link), which lacks the journal pagination and was not compared with the journal text. This project checked the statements of Theorem 1.2 and Proposition 3.1 clause by clause and read the proof of Theorem 1.2 for its structure; that reading warrants nothing here. Formalization: the formalization link is the file src/latest/ErdosProblems/Erdos801.lean of Boris Alexeev's lean-proofs repository at its commit of 15 September 2026, which declares itself a Lean formalization of Alon's solution, names Codex and GPT-5.6 Sol as its formal authors, and proves Erdos801.erdos_801 with explicit constants and the base-two logarithm under the hypothesis G.indepNum ≤ Nat.sqrt n; formal-conjectures names it as the formal proof of its statement file for this problem, added 2026-09-20 and marked research solved. This corpus has not built or audited that development, so no formalized evidence is listed.

Dating. The page is dated by the issue month the journal record gives; the day in the page name is a placeholder, since the preprint carries no date and no earlier posting is known.