Erdős problem 23
The blow-up of shows that the bound in Erdős Problem 23 is tight: any bipartite subgraph must omit at least edges.
Sources
FormalConjectures/ErdosProblems/
23.lean
Retained formal statement
There exists a triangle-free graph on vertices such that at least edges must be removed to make it bipartite. The balanced blow-up of with five parts of size witnesses this.
∃ G, G.CliqueFree 3 ∧ ∀ H ≤ G, H.IsBipartite → 25 ≤ (G.edgeFinset \ H.edgeFinset).cardSolvedStatement only, no proof