The board / graph theory / #1021
Erdős Problem #1021
PROVEDdatabase updated 2026-01-20
The statement as posed is true, and a proof exists.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The graph `G_k`: the bipartite graph between `{y_1, …, y_k}` (the elements of `Fin k`) and `{z_1, …, z_{k choose 2}}` (the two-element subsets of `Fin k`), each `z` being joined to the two elements of the corresponding pair. This is the `1`-subdivision of `K_k`.
Is it true that, for every \(k \geq 3\), there is a constant \(c_k > 0\) such that \[\mathrm{ex}(n, G_k) \ll n^{3/2 - c_k},\] where \(G_k\) is the bipartite graph between \(\{y_1, \ldots, y_k\}\) and \(\{z_1, \ldots, z_{\binom{k}{2}}\}\), with each \(z_j\) joined to a unique pair of \(y_i\)? A conjecture of Erdős and Simonovits [Er71, Er74c], who proved (in unpublished work) that one must have \(c_k \to 0\) as \(k \to \infty\). The graph \(G_k\) is the \(1\)-subdivision of \(K_k\); for \(k = 3\) it is the \(6\)-cycle. This was proved by Conlon and Lee [CoLe21] with \(c_k = 6^{-k}\), improved to \(c_k = \frac{1}{4k - 6}\) by Janzer [Ja19]; see `erdos_1021.variants.janzer`.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/1021.Prizenone
Topicsgraph theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/1021
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.