1. FormalConjectures
  2. ErdosProblems
  3. «23»
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Erdős Problem 23

References:

open SimpleGraph BigOperatorsnamespace Erdos23open scoped Classical in

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.

@[category test, AMS 5] theorem erdos_23.variants.n1 : ∀ (G : SimpleGraph (Fin 5)), G.CliqueFree 3 → ∃ (H : SimpleGraph (Fin 5)), H ≤ G ∧ H.IsBipartite ∧ (G.edgeFinset \ H.edgeFinset).card ≤ 1 := ⊢ ∀ (G : SimpleGraph (Fin 5)), G.CliqueFree 3 → ∃ H ≤ G, H.IsBipartite ∧ (G.edgeFinset \ H.edgeFinset).card ≤ 1 All goals completed! 🐙open scoped Classical in

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.

@[category test, AMS 5] theorem erdos_23.variants.n1_tight : ∃ (G : SimpleGraph (Fin 5)), G.CliqueFree 3 ∧ ∀ (H : SimpleGraph (Fin 5)), H ≤ G → H.IsBipartite → 1 ≤ (G.edgeFinset \ H.edgeFinset).card := ⊢ ∃ G, G.CliqueFree 3 ∧ ∀ H ≤ G, H.IsBipartite → 1 ≤ (G.edgeFinset \ H.edgeFinset).card All goals completed! 🐙open scoped Classical in

Every triangle-free graph on $25$ vertices can be made bipartite by removing at most $25$ edges.

This is the $n = 5$ case of Erdős Problem 23. It follows from the high-density range of Balogh-Clemen-Lidicky together with McKay's complete catalogue of the 23-vertex extremal graphs for bipartization of triangle-free graphs.

@[category research solved, AMS 5] theorem erdos_23.variants.n5 : ∀ (G : SimpleGraph (Fin 25)), G.CliqueFree 3 → ∃ (H : SimpleGraph (Fin 25)), H ≤ G ∧ H.IsBipartite ∧ (G.edgeFinset \ H.edgeFinset).card ≤ 25 := ⊢ ∀ (G : SimpleGraph (Fin 25)), G.CliqueFree 3 → ∃ H ≤ G, H.IsBipartite ∧ (G.edgeFinset \ H.edgeFinset).card ≤ 25 All goals completed! 🐙open scoped Classical in

There exists a triangle-free graph on $25$ vertices such that at least $25$ edges must be removed to make it bipartite. The balanced blow-up of $C_5$ with five parts of size $5$ witnesses this.

@[category research solved, AMS 5] theorem erdos_23.variants.n5_tight : ∃ (G : SimpleGraph (Fin 25)), G.CliqueFree 3 ∧ ∀ (H : SimpleGraph (Fin 25)), H ≤ G → H.IsBipartite → 25 ≤ (G.edgeFinset \ H.edgeFinset).card := ⊢ ∃ G, G.CliqueFree 3 ∧ ∀ H ≤ G, H.IsBipartite → 25 ≤ (G.edgeFinset \ H.edgeFinset).card All goals completed! 🐙

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}$.

def blowupC5 (n : ℕ) : SimpleGraph (ZMod 5 × Fin n) := SimpleGraph.fromRel fun (i, _) (j, _) => i + 1 = j ∨ j + 1 = iopen scoped Classical in

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.

@[category test, AMS 5] theorem 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 := n:ℕ_hn:0 < nH:SimpleGraph (ZMod 5 × Fin n)hH:H ≤ blowupC5 nhBip:H.IsBipartite⊢ n ^ 2 ≤ ((blowupC5 n).edgeFinset \ H.edgeFinset).card All goals completed! 🐙open scoped Classical in

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

@[category research open, AMS 5] theorem erdos_23 : answer(sorry) ↔ ∀ (n : ℕ) (V : Type) [Fintype V], Fintype.card V = 5 * n → ∀ (G : SimpleGraph V), G.CliqueFree 3 → ∃ (H : SimpleGraph V), H ≤ G ∧ H.IsBipartite ∧ (G.edgeFinset \ H.edgeFinset).card ≤ n^2 := ⊢ True ↔ ∀ (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 All goals completed! 🐙-- TODO: add the remaining variants/statements/comments end Erdos23