Turán numbers of bipartite graphs

DefinitionThe \((k-1)\)-subdivision of a graph#✓fully proved

For a simple graph \(H\) on the vertex set \(\{0, \dots, m - 1\}\) and a natural number \(k \ge 2\), the \((k-1)\)-subdivision \(H^{k-1}\) is the graph obtained from \(H\) by replacing each edge \(ij\) with \(i < j\) by a path \(i, (ij, 0), (ij, 1), \dots, (ij, k - 2), j\) of length \(k\) through \(k - 1\) new vertices, the paths of different edges sharing no new vertices. For \(k \le 1\) there are no new vertices and the resulting graph has no edges.

def subdivision {m : ℕ} (H : SimpleGraph (Fin m)) (k : ℕ) :
    SimpleGraph (Fin m ⊕ ({p : Fin m × Fin m // p.1 < p.2 ∧ H.Adj p.1 p.2} × Fin (k - 1))) :=
  SimpleGraph.fromRel fun u v => match u, v with
    | .inl i, .inr (e, t) => e.1.1 = i ∧ (t : ℕ) = 0
    | .inr (e, t), .inr (e', t') => e = e' ∧ (t' : ℕ) = t + 1
    | .inr (e, t), .inl j => e.1.2 = j ∧ (t : ℕ) = k - 2
    | _, _ => False

Used by 1

Used byThe Conlon–Lee subdivision conjecture

DefinitionContaining a copy of a graph#✓fully proved

A simple graph \(G\) contains a copy of a simple graph \(F\) if there is an injective map \(f\) from the vertices of \(F\) to the vertices of \(G\) such that \(f(u)\) and \(f(v)\) are adjacent in \(G\) whenever \(u\) and \(v\) are adjacent in \(F\); the copy need not be induced.

def ContainsCopy {V W : Type} (F : SimpleGraph V) (G : SimpleGraph W) : Prop :=
  ∃ f : V ↪ W, ∀ u v, F.Adj u v → G.Adj (f u) (f v)

Used by 1

Used byThe extremal number of a graph

DefinitionThe extremal number of a graph#✓fully proved

For a natural number \(n\) and a simple graph \(F\), the extremal number \(\mathrm{ex}(n, F)\) is the maximum number of edges of a simple graph on the vertex set \(\{0, \dots, n - 1\}\) that contains no copy of \(F\). It is \(0\) when every simple graph on these \(n\) vertices contains a copy of \(F\).

noncomputable def ex {V : Type} (n : ℕ) (F : SimpleGraph V) : ℕ :=
  sSup {e | ∃ G : SimpleGraph (Fin n), ¬ ContainsCopy F G ∧ G.edgeFinset.card = e}

Uses 1 · Used by 1

Statement usesContaining a copy of a graph

Used byThe Conlon–Lee subdivision conjecture

DefinitionThe Conlon–Lee subdivision conjecture#✓fully proved

For a simple graph \(H\) and a natural number \(k\), write \(H^{k-1}\) for the \((k-1)\)-subdivision of \(H\), and for a simple graph \(F\) and a natural number \(n\) write \(\mathrm{ex}(n, F)\) for the extremal number of \(F\) on \(n\) vertices. The conjecture is the statement that for every even natural number \(k \ge 2\), every natural number \(m\) and every simple graph \(H\) on the vertex set \(\{0, \dots, m - 1\}\), there are real numbers \(\delta > 0\) and \(C\) such that \(\mathrm{ex}(n, H^{k-1}) \le C \cdot n^{1 + 1/k - \delta}\) for every natural number \(n\). In other words, \(\mathrm{ex}(n, H^{k-1}) = O(n^{1 + 1/k - \delta})\) for some \(\delta > 0\).

def conjecture : Prop :=
  ∀ (k m : ℕ) (H : SimpleGraph (Fin m)), 2 ≤ k → Even k → ∃ δ > (0 : ℝ), ∃ C : ℝ, ∀ n : ℕ,
    (ex n (subdivision H k) : ℝ) ≤ C * (n : ℝ) ^ (1 + 1 / (k : ℝ) - δ)

Uses 2 · Used by 1

Statement usesThe extremal number of a graph · The \((k-1)\)-subdivision of a graph

Used byThe Conlon–Lee subdivision conjecture holds

TheoremThe Conlon–Lee subdivision conjecture holds#●ready to prove

For a simple graph \(F\) and a natural number \(n\), let \(\mathrm{ex}(n, F)\) be the maximum number of edges of a simple graph on \(n\) vertices that contains no copy of \(F\) (not necessarily induced), or \(0\) if there is no such graph. For a simple graph \(H\) and a natural number \(k \ge 2\), let \(H^{k-1}\) be the graph obtained from \(H\) by replacing each edge with a path of length \(k\) through \(k - 1\) new vertices (internally disjoint for different edges). Then for every even natural number \(k \ge 2\), every natural number \(m\) and every simple graph \(H\) on the vertex set \(\{0, \dots, m - 1\}\), there are real numbers \(\delta > 0\) and \(C\) such that \(\mathrm{ex}(n, H^{k-1}) \le C \cdot n^{1 + 1/k - \delta}\) for every natural number \(n\).

This was proved by Janzer (Bull. London Math. Soc. 53 (2021) 108–118, Theorem 1.7).

public theorem_wanted conjecture_holds : conjecture

Sources

• O. Janzer, The extremal number of longer subdivisions, Bull. London Math. Soc. 53 (2021) 108-118, arXiv:1905.08001, https://doi.org/10.1112/blms.12404.

Uses 1

Statement usesThe Conlon–Lee subdivision conjecture

DefinitionErdős–Simonovits degeneracy conjecture (Erdős Problem 146)#✓fully proved

The statement that for every finite simple graph \(H\) and every natural number \(r \ge 1\), if \(H\) is bipartite and \(r\)-degenerate (every nonempty set of vertices contains a vertex with at most \(r\) neighbours in that set), then \(\mathrm{ex}(n; H) = O(n^{2 - 1/r})\) as \(n \to \infty\), where \(\mathrm{ex}(n; H)\) is the largest number of edges of a simple graph on \(n\) vertices containing no copy of \(H\).

def DegenerateExtremalClaim : Prop :=
  ∀ (V : Type*) [Fintype V] (H : SimpleGraph V) (r : ℕ),
    H.IsBipartite → H.IsDegenerate r → 1 ≤ r →
      Asymptotics.IsBigO Filter.atTop
        (fun n : ℕ => (SimpleGraph.extremalNumber n H : ℝ))
        (fun n : ℕ => (n : ℝ) ^ ((2 : ℝ) - 1 / (r : ℝ)))

Uses 1 · Used by 1

Statement usesDegenerate graph

Used byCounterexample to the Erdős–Simonovits degeneracy conjecture

TheoremCounterexample to the Erdős–Simonovits degeneracy conjecture#●ready to prove

It is not true that for every finite simple graph \(H\) and every natural number \(r \ge 1\) such that \(H\) is bipartite and \(r\)-degenerate (every nonempty set of vertices contains a vertex with at most \(r\) neighbours in that set), the extremal number \(\mathrm{ex}(n; H)\) (the largest number of edges of a simple graph on \(n\) vertices containing no copy of \(H\)) is \(O(n^{2 - 1/r})\) as \(n \to \infty\).

An internal OpenAI model constructed a connected bipartite \(2\)-degenerate graph \(H\) with \(\mathrm{ex}(n; H) \ge c n^{3/2 + \varepsilon}\) for all large \(n\), for some constants \(c > 0\) and \(\varepsilon > 0\); erdosproblems.com/146 records the conjecture as disproved.

public theorem_wanted DegenerateExtremalClaim_refuted : ¬ EP146.DegenerateExtremalClaim

Sources

• T. F. Bloom, Erdős Problem #146, erdosproblems.com (live page, LaTeX source and forum threads read 2026-10-22), https://www.erdosproblems.com/146; OpenAI, Ten proofs (section disproving the Erdős degeneracy conjecture), 2026, https://cdn.openai.com/pdf/ten-proofs-oai.pdf.

Uses 1

Statement usesErdős–Simonovits degeneracy conjecture (Erdős Problem 146)

5 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.