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.

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

23.lean

Retained formal statement3 of 6

Every triangle-free graph on $5$ vertices can be made bipartite by removing at most $1$ edge. This is the $n = 1$ case of Erdős Problem 23.

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

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

TestStatement only, no proof