---

Claim. The answer to Problem 926 is yes: for every fixed $k\ge4$, $\mathrm{ex}(n;H_k)\ll_k n^{3/2}$. The claimed result is Theorem 1.4 of Z. Füredi, On a Turán type problem of Erdős, Combinatorica 11 (1991), no. 1, 75--79 (printed p. 76): for integers $n\ge1$, $k\ge2$ and $s\ge1$, the bipartite graph $L^{k,s}$ with vertices $x_0$, $y_1,\dots,y_k$ and $x_{ij}^\alpha$ ($1\le i<j\le k$, $1\le\alpha\le s$), and edges $x_0y_i$, $x_{ij}^\alpha y_i$ and $x_{ij}^\alpha y_j$, satisfies

$$\mathrm{ex}(n;L^{k,s})<\frac{n(k-1)}4+n^{3/2}\sqrt{\frac{sk(k-1)^2+2(k-2)(k-1)}8}.$$

At $s=1$ the graph $L^{k,1}$ is the problem's $H_k$, under the reading that assigns a separate vertex $z_{\{i,j\}}$ to each unordered pair of the $y_i$: identify $x$ with $x_0$, each $y_i$ with itself and $z_{\{i,j\}}$ with $x_{ij}^1$. The bound is then $O(k^{3/2}n^{3/2})$, so for fixed $k$ it is $O_k(n^{3/2})$, the bound asked for; the abstract states the simpler sufficient condition that $k^{3/2}n^{3/2}$ edges force a copy of $L^k$. The exponent is right: blowing up each vertex of an extremal $C_4$-free graph into $k-1$ vertices gives $L^k$-free graphs with $(1+o(1))\frac{\sqrt{k-1}}2n^{3/2}$ edges, as the paper notes. The paper presents the theorem as a step toward Erdős's conjecture that every bipartite graph whose induced subgraphs all have a vertex of degree at most $2$ has extremal number $O(n^{3/2})$; the problem asks only about the family $H_k$, and the dependence on $k$, which Alon, Krivelevich and Sudakov later improved (their claim page), is not part of the question.

Acceptance. Reviewed: the site's curator, Thomas Bloom, labels the problem proved and credits this paper with the answer yes and the bound $\mathrm{ex}(n;H_k)\ll(kn)^{3/2}$; Füredi had no part in that entry. Refereed: Combinatorica (Crossref record accessed: volume 11, issue 1, pp. 75--79, issued March 1991; the day is the issue's nominal first day, used for this page's date). The source has a library source card. Read depth: printed pp. 75--77 for the definitions, the statement of Theorem 1.4 and its proof pointer; the proof, through the set-system Lemma 1.5, is not checked. The acceptance rests on the publication and the curator's acceptance; nothing is independently reviewed by this project; the site's label is the discussion link.

Formalization. The file src/latest/ErdosProblems/Erdos926.lean of Boris Alexeev's repository plby/lean-proofs (linked above at the commit that the formal-conjectures statement file pins; in the repository since 2026-08-17) declares itself a Lean formalization of a solution to the problem, naming Zoltán Füredi as its informal author and, as formal authors, the AI systems Codex and GPT-5.6 Sol. Its docstring says that it proves an explicit Füredi-type estimate for every finite $H_k$-free graph and deduces $\mathrm{ex}(n,H_k)=O_k(n^{3/2})$, with $H_k$ built from one center, $k$ branch vertices and one vertex for every pair of branches, the distinct-pair reading. The formal-conjectures statement erdos_926 names the file in its formal_proof attribute (the problem page records that file). This project has not built, replayed or audited it, so the page lists no formalized evidence.