---

The claim. Proposition 2.1 of N. Alon, Problems and results in extremal combinatorics---II, Discrete Math. 308 (2008), no. 19, 4460--4472, with logarithms in base $2$: for every $D>1$ and every $n>10^5$ there is a graph $G$ with at most $2n$ vertices and at least $2n\log(2n)$ edges such that every subgraph $H$ of $G$ on $m$ vertices with average degree at least $d$ and maximum degree at most $Dd$ has $d<36(4\sqrt{\log m}+\log(64D)+18)$. Section 2, after printing the problem, says that the Erdős--Simonovits question is not true, and Janzer and Sudakov's Theorem 6.2 calls the result a negative answer to it: no absolute constants $\epsilon$ and $D$ satisfy the statement of Problem 803. The construction, a random bipartite graph with a class of $n$ vertices each joined to one random vertex of each of the classes $B_{i,j}$ of $n/2^i$ vertices, modifies that of Pyber, Rödl and Szemerédi.

The near-matching positive result is Janzer and Sudakov's Theorem 6.3 (Forum Math. Pi 11 (2023), e19), which gives a $64$-almost-regular subgraph on $m\ge m_0$ vertices with $\varepsilon(m_0)m\sqrt{\log m}/(\log\log m)^{3/2}$ edges in every graph with $n\ge n_0(m_0)$ vertices and $n\log n$ edges, so Alon's bound is tight up to $\log\log$ factors. It proves a weaker statement than the one asked and settles nothing of the question, so it is recorded on the problem page and has no claim page.

What the corpus holds. The author's preprint (pdfTeX of 17 September 2007, 16 pages) on the source card, paged at Proposition 2.1, which states the definition, the printed problem and the proposition from p. 2 of the preprint. The journal text is not held.

Acceptance. Refereed: Discrete Mathematics, volume 308, issue 19 (Crossref dates the issue October 2008). Reviewed: Janzer and Sudakov's refereed paper quotes the result as its Theorem 6.2 and calls it a negative answer to the question, and the site's curator, T. F. Bloom, credits Alon with the disproof in the problem's commentary (erdosproblems.com/803, last edited 7 October 2025; label DISPROVED on 2026-09-18 and none printed to an anonymous reader on 2026-10-07; "Formalised statement? Yes" on 2026-10-07; no comment and no proof claim on the site). Janzer and Sudakov print the bound without the factor $m$ on two of its three terms; the problem page records the two forms.

Formalizations. Two third-party Lean developments declare themselves formalizations of this result. The corpus has built and audited neither, so they are formalization links and the evidence stays reviewed and refereed. (1) Erdos803.lean in Boris Alexeev's lean-proofs repository (the first formalization link, pinned): its header names Noga Alon as informal author and Codex and GPT-5.6 Sol as formal authors. Its theorem not_erdos_803 refutes the statement with absolute constants $\epsilon>0$ and $D\ge1$, every $m\ge1$ and all large $n$ (the site's form, with natural logarithms) by a counting argument that is not Alon's: for a fixed $m$ with $\epsilon\log m>6$ and infinitely many $n$ it builds a graph with at least $n\log n$ edges in which every $m$ vertices span fewer than $6m$ edges, so no $m$-vertex subgraph, balanced or not, has $\epsilon m\log m$ edges; Alon's construction appears only in the file's accompanying plan. The statement file ErdosProblems/803.lean of formal-conjectures, added on 2026-09-20, names this theorem as the formal proof of its erdos_803. (2) Collin Yuanjie Ren's package for the problem (the second formalization link, pinned; its README says the code was prepared with Claude Code), which the community database lists as the problem's Lean formalization, an entry its file has carried since 26 September 2026 (dated 16 September 2026 in the entry): its alon_construction is Alon's Proposition 2.1 with the edge bound $18m(4\sqrt{\log_2m}+\log_2(64D)+26)$ (the additive constant $26$ in place of $18$, from an integer threshold), and not_erdosSimonovitsUniform and not_erdosSimonovitsLiteral are the negative answers in the 1970 reading (at least $m_0$ vertices) and in the site's reading (exactly $m$ vertices). The README reports the three theorems built with the axioms propext, Classical.choice and Quot.sound only.