Erdős problem 23 · problems.science

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.

Sources

Browse retained paths and inspect the exact material available for this Problem.

6 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

23.lean

Retained formal statement5 of 6

Every triangle-free graph on $25$ vertices can be made bipartite by removing at most $25$ edges.

This is the $n = 5$ case of Erdős Problem 23. It follows from the high-density range of Balogh-Clemen-Lidicky together with McKay's complete catalogue of the 23-vertex extremal graphs for bipartization of triangle-free graphs.

FormalConjectures/ErdosProblems/23.leanErdos23.erdos_23.variants.n51 lineExact file

1∀ (G : SimpleGraph (Fin 25)), G.CliqueFree 3 → ∃ H ≤ G, H.IsBipartite ∧ (G.edgeFinset \ H.edgeFinset).card ≤ 25

SolvedStatement only, no proof

Sources

Search problems.science