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

Can every triangle-free graph on $5n$ vertices be made bipartite by deleting at most $n^2$ edges?

FormalConjectures/ErdosProblems/23.leanErdos23.erdos_234 linesExact file

1sorry ↔2  ∀ (n : ℕ) (V : Type) [inst : Fintype V],3    Fintype.card V = 5 * n →4      ∀ (G : SimpleGraph V), G.CliqueFree 3 → ∃ H ≤ G, H.IsBipartite ∧ (G.edgeFinset \ H.edgeFinset).card ≤ n ^ 2

OpenStatement only, no proof

Sources

Search problems.science