---

Claim. The answer to Problem 1021 is yes, with $c_k=1/(4k-6)$: for every fixed $k\ge3$ there is $C_k$ such that

$$\mathrm{ex}(n,G_k)\le C_kn^{1+(k-2)/(2k-3)}=C_kn^{3/2-1/(4k-6)}.$$

The claimed result is Theorem 3 of O. Janzer, Improved bounds for the extremal number of subdivisions, Electron. J. Combin. 26 (2019), no. 3, Paper P3.3, 6 pp., DOI 10.37236/8262 (published 5 July 2019, the paper link's date; submitted 24 October 2018 and accepted 10 June 2019, as the first page of the journal version prints), stated for the one-subdivision $H_t$ of $K_t$ and recorded clause by clause on the result page Theorem 3 (p. 2; card). The graph $G_k$ is $H_k$, as the problem page writes out under Progress. The paper derives Theorem 3 from its Theorem 4, the same exponent for the one-subdivision of $K_{s+t-1}$ minus the edges of a $K_s$, by taking $s=1$; the reciprocal of the gap, $4k-6$, grows linearly in $k$. At $k=3$ the graph is $C_6$ and the exponent $4/3$ is the known order of $\mathrm{ex}(n,C_6)$, so the bound is tight there; no sharpness for larger $k$ is claimed by the paper.

Depends on. Nothing in this wiki as a premise. The proof reuses two lemmas of Conlon and Lee (their Lemmas 2.3 and 2.4, cited as the paper's Lemmas 6 and 8), not their Theorem 5.1, which this result sharpens.

Formalization. The file src/latest/ErdosProblems/Erdos1021.lean of Boris Alexeev's plby/lean-proofs repository, at the commit linked above (the file was added on 17 August 2026), opens by calling itself a Lean formalization of a solution to Problem 1021, names Janzer as the informal author and Codex and GPT-5.6 Sol as the formal authors, as the file names them, and says it proves $\mathrm{ex}(n,\mathrm{cliqueSubdivision}\,k)=O(n^{3/2-1/(4k-6)})$. Its cliqueSubdivision_extremal_upper is that bound for each $k\ge3$, and its final theorem erdos_1021 (line 2359) gives, for every $k\ge3$, a positive $c$ with $\mathrm{ex}(n,G_k)=O(n^{3/2-c})$, the question's literal form. The formal-conjectures statement file ErdosProblems/1021.lean, added on 19 September 2026, points its erdos_1021 and erdos_1021.variants.janzer to this file and is a statement, not a formalization link. This corpus has not built the development or printed its axioms; the link above pins the commit. The development is therefore a link on this page, and evidence stays reviewed and refereed.

Acceptance. Refereed publication in the Electronic Journal of Combinatorics, cited with its venue above, the refereed evidence. The reviewed evidence is the documented acceptance of the site's curator, Thomas Bloom, who took no part in the paper: the site's commentary names the paper as the improvement to $c_k=1/(4k-6)$ of the Conlon--Lee proof; the forum comment of 13 September 2025 calling it the best bound (through the restatement in Conlon, Janzer and Lee's later paper, arXiv:1903.10631, its Theorem 1.5) is marked by the site as addressed. This page's date is the arXiv v1 posting, 3 September 2018 (arXiv record, 2026-10-07); the five-page arXiv manuscript was not compared with the six-page journal version. Read depth: pp. 1--3 and 5--6 of the journal version are the basis for the definitions, the statements, the reduction to Theorem 4 and the proof's endpoint; p. 4 and the full argument were not checked, and nothing is independently reviewed by this project.