Skip to content

Erdős problem 23

Start work

The blow-up of C5C_5 shows that the bound n2n^2 in Erdős Problem 23 is tight: any bipartite subgraph must omit at least n2n^2 edges.

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

23.lean

Retained formal statement2 of 6

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

FormalConjectures/ErdosProblems/23.leanErdos23.erdos_234 linesExact file
sorry ↔  ∀ (n : ℕ) (V : Type) [inst : Fintype V],    Fintype.card V = 5 * n →      ∀ (G : SimpleGraph V), G.CliqueFree 3 → ∃ H ≤ G, H.IsBipartite ∧ (G.edgeFinset \ H.edgeFinset).card ≤ n ^ 2
OpenStatement only, no proof