Erdős Problem 23

References:

• erdosproblems.com/23
• OEIS A389646

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

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.

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

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.

def Erdos23.blowupC5 (n : ℕ) : SimpleGraph (ZMod 5 × Fin n)

The blow-up of the 5-cycle $C_5$: replace each vertex of $C_5$ with an independent set of $n$ vertices, and connect two vertices iff their corresponding vertices in $C_5$ are adjacent. The vertex set is $\mathbb{Z}/5\mathbb{Z} \times \{0, \ldots, n-1\}$, where $(i, a)$ and $(j, b)$ are adjacent iff $j = i + 1$ or $i = j + 1$ in $\mathbb{Z}/5\mathbb{Z}$.

Equations

• Erdos23.blowupC5 n = SimpleGraph.fromRel fun (x x_1 : ZMod 5 × Fin n) => match x with | (i, snd) => match x_1 with | (j, snd) => i + 1 = j ∨ j + 1 = i

theorem Erdos23.blowupC5_tight (n : ℕ) (_hn : 0 < n) (H : SimpleGraph (ZMod 5 × Fin n)) (hH : H ≤ blowupC5 n) (hBip : H.IsBipartite) : n ^ 2 ≤ ((blowupC5 n).edgeFinset \ H.edgeFinset).card

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.

theorem Erdos23.erdos_23 : 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

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