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 statement4 of 6

There exists a triangle-free graph on $5$ vertices such that at least $1$ edge must be removed to make it bipartite. This shows the bound in erdos_23_n1 is tight.

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

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

TestStatement only, no proof

Sources

Search problems.science