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 BigOperators Classical namespace Erdos23

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 declaration uses 'sorry'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! 🐙

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 declaration uses 'sorry'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! 🐙

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 declaration uses 'sorry'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! 🐙

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 declaration uses 'sorry'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 = i

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 declaration uses 'sorry'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! 🐙

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

@[category research open, AMS 5] theorem declaration uses 'sorry'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