Erdős problem 146

If $H$ is bipartite and $r$ -degenerate, is $\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

FormalConjectures/ErdosProblems/

146.lean

Retained formal statement2 of 2

The counterexample: a connected bipartite 2-degenerate H whose extremal number exceeds $n^{3/2+\epsilon}$ infinitely often, so the r = 2 case of erdos_146 fails.

FormalConjectures/ErdosProblems/146.leanErdos146.erdos_146.variants.two_degenerate_counterexample5 linesExact file

1∃ q H,2  H.Connected ∧3    H.IsBipartite ∧4      Erdos146.IsDegenerate 2 H ∧5        ∃ c ε, 0 < c ∧ 0 < ε ∧ ∀ᶠ (n : ℕ) in Filter.atTop, c * ↑n ^ (3 / 2 + ε) ≤ ↑(SimpleGraph.extremalNumber n H)

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.