Skip to content

Erdős problem 146

If HH is bipartite and rr-degenerate, is ex(n;H)≪n2−1/r\mathrm{ex}(n;H) \ll n^{2-1/r} (a $500 Erdős-Simonovits prize conjecture)? A counterexample refutes the degeneracy conjecture.

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

146.lean

Retained formal statement1 of 2

If HH is bipartite and is rr-degenerate, that is, every induced subgraph of HH has minimum degree ≤r\leq r, then ex(n;H)≪n2−1/r.\mathrm{ex}(n;H) \ll n^{2-1/r}.

The answer is no. OpenAI [OpenAI26] give a connected bipartite 2-degenerate H and constants c, ε > 0 with ex(n;H)≥cn3/2+ϵ\mathrm{ex}(n;H)\geq cn^{3/2+\epsilon} for all large n, which exceeds the conjectured n2−1/2=n3/2n^{2-1/2}=n^{3/2}. See erdos_146.variants.two_degenerate_counterexample.

FormalConjectures/ErdosProblems/146.leanErdos146.erdos_1466 linesExact file
False ↔  ∀ (r q : ℕ) (H : SimpleGraph (Fin q)),    0 < r →      H.IsBipartite →        Erdos146.IsDegenerate r H →          (fun n => ↑(SimpleGraph.extremalNumber n H)) =O[Filter.atTop] fun n => ↑n ^ (2 - 1 / ↑r)
SolvedStatement only, no proof