Erdős problem 23

The blow-up of $C_5$ shows that the bound $n^2$ in Erdős Problem 23 is tight: any bipartite subgraph must omit at least $n^2$ edges.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

FormalConjectures/ErdosProblems/23.lean

Formal Conjectures

FormalConjectures/ErdosProblems/23.leanErdos23.blowupC5_tight2 linesExact file

1∀ (n : ℕ),2  0 < n → ∀ H ≤ Erdos23.blowupC5 n, H.IsBipartite → n ^ 2 ≤ ((Erdos23.blowupC5 n).edgeFinset \ H.edgeFinset).card

TestStatement only, no proof