1. FormalConjectures
  2. ErdosProblems
  3. «74»
/- Copyright 2025 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 74

Reference: erdosproblems.com/74

open Filter SimpleGraph open scoped Topology Real namespace Erdos74 open Erdos74 universe uvariable {V : Type u}

For a given subgraph A, this is the set of all numbers k such that A can be made bipartite by deleting k edges.

def SimpleGraph.edgeDistancesToBipartite {G : SimpleGraph V} (A : G.Subgraph) : Set ℕ := { (E.ncard) | (E : Set (Sym2 V)) (_ : E ⊆ A.edgeSet) (_ : IsBipartite (A.deleteEdges E).coe)}

The set of edge distances to a bipartite graph is always non-empty because deleting all edges from a graph makes it bipartite.

@[category test, AMS 5] theorem SimpleGraph.edgeDistancesToBipartite_nonempty {G : SimpleGraph V} (A : G.Subgraph) : SimpleGraph.edgeDistancesToBipartite A |>.Nonempty := V:Type uG:SimpleGraph VA:G.Subgraph⊢ (edgeDistancesToBipartite A).Nonempty V:Type uG:SimpleGraph VA:G.Subgraph⊢ {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x}.Nonempty V:Type uG:SimpleGraph VA:G.Subgraph⊢ (A.deleteEdges A.edgeSet).coe.IsBipartite V:Type uG:SimpleGraph VA:G.Subgraph⊢ ∀ {a b : ↑(A.deleteEdges A.edgeSet).verts}, (A.deleteEdges A.edgeSet).coe.Adj a b → (completeGraph (Fin 2)).Adj 0 0 All goals completed! 🐙

The minimum number of edges that must be deleted from a subgraph A to make it bipartite.

noncomputable def SimpleGraph.minEdgeDistToBipartite {G : SimpleGraph V} (A : G.Subgraph) : ℕ := sInf <| SimpleGraph.edgeDistancesToBipartite A

For a graph G and a number n, this is the set of minEdgeDistToBipartite A for all induced subgraphs A of G on n vertices.

def SimpleGraph.subgraphEdgeDistsToBipartite (G : SimpleGraph V) (n : ℕ) : Set ℕ := { (SimpleGraph.minEdgeDistToBipartite A) | (A : Subgraph G) (_ : A.verts.ncard = n) (_ : A.verts.Finite) }

The set of minimum edge distances to bipartite for subgraphs of size n is bounded above. A graph on n vertices has at most n choose 2 edges, and deleting all of them makes the graph bipartite, providing a straightforward upper bound.

@[category test, AMS 5] theorem SimpleGraph.subgraphEdgeDistsToBipartite_bddAbove (G : SimpleGraph V) (n : ℕ) : BddAbove (SimpleGraph.subgraphEdgeDistsToBipartite G n) := V:Type uG:SimpleGraph Vn:ℕ⊢ BddAbove (subgraphEdgeDistsToBipartite G n) V:Type uG:SimpleGraph Vn:ℕ⊢ n.choose 2 ∈ upperBounds (subgraphEdgeDistsToBipartite G n) V:Type uG:SimpleGraph Vn:ℕ⊢ ∀ ⦃a : ℕ⦄, (∃ A, ∃ (_ : A.verts.ncard = n) (_ : A.verts.Finite), sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = a) → a ≤ n.choose 2 intro m V:Type uG:SimpleGraph Vn:ℕm:ℕh:∃ A, ∃ (_ : A.verts.ncard = n) (_ : A.verts.Finite), sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = m⊢ m ≤ n.choose 2 V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = m⊢ m ≤ n.choose 2 V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = m⊢ sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} ≤ n.choose 2 have : A.edgeSet.ncard ≤ n.choose 2 := V:Type uG:SimpleGraph Vn:ℕ⊢ BddAbove (subgraphEdgeDistsToBipartite G n) V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = m⊢ A.edgeSet.ncard ≤ A.verts.ncard.choose 2 V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis:Fintype ↑A.verts := h_fin.fintype⊢ A.edgeSet.ncard ≤ A.verts.ncard.choose 2 V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis✝:Fintype ↑A.verts := h_fin.fintypethis:Fintype ↑A.coe.edgeSet := Fintype.ofFinite ↑A.coe.edgeSet⊢ A.edgeSet.ncard ≤ A.verts.ncard.choose 2 V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis✝:Fintype ↑A.verts := h_fin.fintypethis:Fintype ↑A.coe.edgeSet := Fintype.ofFinite ↑A.coe.edgeSet⊢ A.edgeSet.ncard = A.coe.edgeFinset.cardV:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis✝:Fintype ↑A.verts := h_fin.fintypethis:Fintype ↑A.coe.edgeSet := Fintype.ofFinite ↑A.coe.edgeSet⊢ A.verts.ncard = Fintype.card ↑A.verts V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis✝:Fintype ↑A.verts := h_fin.fintypethis:Fintype ↑A.coe.edgeSet := Fintype.ofFinite ↑A.coe.edgeSet⊢ A.edgeSet.ncard = A.coe.edgeFinset.card V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis✝:Fintype ↑A.verts := h_fin.fintypethis:Fintype ↑A.coe.edgeSet := Fintype.ofFinite ↑A.coe.edgeSet⊢ (Sym2.map Subtype.val '' A.coe.edgeSet).ncard = A.coe.edgeSet.ncard All goals completed! 🐙 V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis✝:Fintype ↑A.verts := h_fin.fintypethis:Fintype ↑A.coe.edgeSet := Fintype.ofFinite ↑A.coe.edgeSet⊢ A.verts.ncard = Fintype.card ↑A.verts All goals completed! 🐙 V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis:A.edgeSet.ncard ≤ n.choose 2 := Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard ≤ _a.choose 2) (Eq.symm hn))) (have this := h_fin.fintype; have this_1 := Fintype.ofFinite ↑A.coe.edgeSet; Eq.mpr (eq_of_heq ((fun α self a a' e'_3 a_1 a'_1 e'_4 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a'_1)) (fun e_3 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_4 ≍ x → (a ≤ a_1) ≍ (a ≤ a'_1)) e'_4 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_4 : a_1 = a'), e_4 ≍ Eq.refl a_1 → (a ≤ a_1) ≍ (a ≤ a')) (fun e_4 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_4) (Eq.refl a'_1) (HEq.refl e'_4)) (Eq.symm h) e'_3) (Eq.refl a') (HEq.refl e'_3)) ℕ instLENat A.edgeSet.ncard A.coe.edgeFinset.card (Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard = _a) (Eq.symm (Set.ncard_coe_finset A.coe.edgeFinset)))) (Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard = _a.ncard) (coe_edgeFinset A.coe))) (Eq.mpr (id (congrArg (fun _a => _a.ncard = A.coe.edgeSet.ncard) (Eq.symm (Subgraph.image_coe_edgeSet_coe A)))) ((Set.ncard_image_iff (Set.toFinite A.coe.edgeSet)).mpr (Function.Injective.injOn (Sym2.map.injective Subtype.coe_injective)))))) (A.verts.ncard.choose 2) ((Fintype.card ↑A.verts).choose 2) (eq_of_heq ((fun a a' e'_1 a_1 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_1 ≍ x → a.choose a_1 ≍ a'.choose a_1) e'_1 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_1 : a = a'), e_1 ≍ Eq.refl a → a.choose a_1 ≍ a'.choose a_1) (fun e_1 h => HEq.refl (a.choose a_1)) (Eq.symm h) e'_1) (Eq.refl a') (HEq.refl e'_1)) A.verts.ncard (Fintype.card ↑A.verts) (Eq.mpr (id (congrArg (fun _a => _a = Fintype.card ↑A.verts) (Set.ncard_eq_toFinset_card A.verts h_fin))) (Eq.mpr (id (congrArg (fun _a => _a = Fintype.card ↑A.verts) (Set.Finite.card_toFinset h_fin))) (Eq.refl (Fintype.card ↑A.verts)))) 2)))) card_edgeFinset_le_card_choose_two)⊢ sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} ≤ A.edgeSet.ncard V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis:A.edgeSet.ncard ≤ n.choose 2 := Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard ≤ _a.choose 2) (Eq.symm hn))) (have this := h_fin.fintype; have this_1 := Fintype.ofFinite ↑A.coe.edgeSet; Eq.mpr (eq_of_heq ((fun α self a a' e'_3 a_1 a'_1 e'_4 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a'_1)) (fun e_3 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_4 ≍ x → (a ≤ a_1) ≍ (a ≤ a'_1)) e'_4 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_4 : a_1 = a'), e_4 ≍ Eq.refl a_1 → (a ≤ a_1) ≍ (a ≤ a')) (fun e_4 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_4) (Eq.refl a'_1) (HEq.refl e'_4)) (Eq.symm h) e'_3) (Eq.refl a') (HEq.refl e'_3)) ℕ instLENat A.edgeSet.ncard A.coe.edgeFinset.card (Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard = _a) (Eq.symm (Set.ncard_coe_finset A.coe.edgeFinset)))) (Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard = _a.ncard) (coe_edgeFinset A.coe))) (Eq.mpr (id (congrArg (fun _a => _a.ncard = A.coe.edgeSet.ncard) (Eq.symm (Subgraph.image_coe_edgeSet_coe A)))) ((Set.ncard_image_iff (Set.toFinite A.coe.edgeSet)).mpr (Function.Injective.injOn (Sym2.map.injective Subtype.coe_injective)))))) (A.verts.ncard.choose 2) ((Fintype.card ↑A.verts).choose 2) (eq_of_heq ((fun a a' e'_1 a_1 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_1 ≍ x → a.choose a_1 ≍ a'.choose a_1) e'_1 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_1 : a = a'), e_1 ≍ Eq.refl a → a.choose a_1 ≍ a'.choose a_1) (fun e_1 h => HEq.refl (a.choose a_1)) (Eq.symm h) e'_1) (Eq.refl a') (HEq.refl e'_1)) A.verts.ncard (Fintype.card ↑A.verts) (Eq.mpr (id (congrArg (fun _a => _a = Fintype.card ↑A.verts) (Set.ncard_eq_toFinset_card A.verts h_fin))) (Eq.mpr (id (congrArg (fun _a => _a = Fintype.card ↑A.verts) (Set.Finite.card_toFinset h_fin))) (Eq.refl (Fintype.card ↑A.verts)))) 2)))) card_edgeFinset_le_card_choose_two)⊢ A.edgeSet.ncard ∈ {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis:A.edgeSet.ncard ≤ n.choose 2 := Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard ≤ _a.choose 2) (Eq.symm hn))) (have this := h_fin.fintype; have this_1 := Fintype.ofFinite ↑A.coe.edgeSet; Eq.mpr (eq_of_heq ((fun α self a a' e'_3 a_1 a'_1 e'_4 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a'_1)) (fun e_3 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_4 ≍ x → (a ≤ a_1) ≍ (a ≤ a'_1)) e'_4 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_4 : a_1 = a'), e_4 ≍ Eq.refl a_1 → (a ≤ a_1) ≍ (a ≤ a')) (fun e_4 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_4) (Eq.refl a'_1) (HEq.refl e'_4)) (Eq.symm h) e'_3) (Eq.refl a') (HEq.refl e'_3)) ℕ instLENat A.edgeSet.ncard A.coe.edgeFinset.card (Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard = _a) (Eq.symm (Set.ncard_coe_finset A.coe.edgeFinset)))) (Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard = _a.ncard) (coe_edgeFinset A.coe))) (Eq.mpr (id (congrArg (fun _a => _a.ncard = A.coe.edgeSet.ncard) (Eq.symm (Subgraph.image_coe_edgeSet_coe A)))) ((Set.ncard_image_iff (Set.toFinite A.coe.edgeSet)).mpr (Function.Injective.injOn (Sym2.map.injective Subtype.coe_injective)))))) (A.verts.ncard.choose 2) ((Fintype.card ↑A.verts).choose 2) (eq_of_heq ((fun a a' e'_1 a_1 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_1 ≍ x → a.choose a_1 ≍ a'.choose a_1) e'_1 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_1 : a = a'), e_1 ≍ Eq.refl a → a.choose a_1 ≍ a'.choose a_1) (fun e_1 h => HEq.refl (a.choose a_1)) (Eq.symm h) e'_1) (Eq.refl a') (HEq.refl e'_1)) A.verts.ncard (Fintype.card ↑A.verts) (Eq.mpr (id (congrArg (fun _a => _a = Fintype.card ↑A.verts) (Set.ncard_eq_toFinset_card A.verts h_fin))) (Eq.mpr (id (congrArg (fun _a => _a = Fintype.card ↑A.verts) (Set.Finite.card_toFinset h_fin))) (Eq.refl (Fintype.card ↑A.verts)))) 2)))) card_edgeFinset_le_card_choose_two)⊢ ∃ E ⊆ A.edgeSet, (A.deleteEdges E).coe.IsBipartite ∧ E.ncard = A.edgeSet.ncard V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis:A.edgeSet.ncard ≤ n.choose 2 := Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard ≤ _a.choose 2) (Eq.symm hn))) (have this := h_fin.fintype; have this_1 := Fintype.ofFinite ↑A.coe.edgeSet; Eq.mpr (eq_of_heq ((fun α self a a' e'_3 a_1 a'_1 e'_4 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a'_1)) (fun e_3 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_4 ≍ x → (a ≤ a_1) ≍ (a ≤ a'_1)) e'_4 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_4 : a_1 = a'), e_4 ≍ Eq.refl a_1 → (a ≤ a_1) ≍ (a ≤ a')) (fun e_4 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_4) (Eq.refl a'_1) (HEq.refl e'_4)) (Eq.symm h) e'_3) (Eq.refl a') (HEq.refl e'_3)) ℕ instLENat A.edgeSet.ncard A.coe.edgeFinset.card (Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard = _a) (Eq.symm (Set.ncard_coe_finset A.coe.edgeFinset)))) (Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard = _a.ncard) (coe_edgeFinset A.coe))) (Eq.mpr (id (congrArg (fun _a => _a.ncard = A.coe.edgeSet.ncard) (Eq.symm (Subgraph.image_coe_edgeSet_coe A)))) ((Set.ncard_image_iff (Set.toFinite A.coe.edgeSet)).mpr (Function.Injective.injOn (Sym2.map.injective Subtype.coe_injective)))))) (A.verts.ncard.choose 2) ((Fintype.card ↑A.verts).choose 2) (eq_of_heq ((fun a a' e'_1 a_1 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_1 ≍ x → a.choose a_1 ≍ a'.choose a_1) e'_1 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_1 : a = a'), e_1 ≍ Eq.refl a → a.choose a_1 ≍ a'.choose a_1) (fun e_1 h => HEq.refl (a.choose a_1)) (Eq.symm h) e'_1) (Eq.refl a') (HEq.refl e'_1)) A.verts.ncard (Fintype.card ↑A.verts) (Eq.mpr (id (congrArg (fun _a => _a = Fintype.card ↑A.verts) (Set.ncard_eq_toFinset_card A.verts h_fin))) (Eq.mpr (id (congrArg (fun _a => _a = Fintype.card ↑A.verts) (Set.Finite.card_toFinset h_fin))) (Eq.refl (Fintype.card ↑A.verts)))) 2)))) card_edgeFinset_le_card_choose_two)⊢ A.edgeSet ⊆ A.edgeSet ∧ (A.deleteEdges A.edgeSet).coe.IsBipartite ∧ A.edgeSet.ncard = A.edgeSet.ncard refine ⟨V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis:A.edgeSet.ncard ≤ n.choose 2 := Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard ≤ _a.choose 2) (Eq.symm hn))) (have this := h_fin.fintype; have this_1 := Fintype.ofFinite ↑A.coe.edgeSet; Eq.mpr (eq_of_heq ((fun α self a a' e'_3 a_1 a'_1 e'_4 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a'_1)) (fun e_3 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_4 ≍ x → (a ≤ a_1) ≍ (a ≤ a'_1)) e'_4 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_4 : a_1 = a'), e_4 ≍ Eq.refl a_1 → (a ≤ a_1) ≍ (a ≤ a')) (fun e_4 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_4) (Eq.refl a'_1) (HEq.refl e'_4)) (Eq.symm h) e'_3) (Eq.refl a') (HEq.refl e'_3)) ℕ instLENat A.edgeSet.ncard A.coe.edgeFinset.card (Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard = _a) (Eq.symm (Set.ncard_coe_finset A.coe.edgeFinset)))) (Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard = _a.ncard) (coe_edgeFinset A.coe))) (Eq.mpr (id (congrArg (fun _a => _a.ncard = A.coe.edgeSet.ncard) (Eq.symm (Subgraph.image_coe_edgeSet_coe A)))) ((Set.ncard_image_iff (Set.toFinite A.coe.edgeSet)).mpr (Function.Injective.injOn (Sym2.map.injective Subtype.coe_injective)))))) (A.verts.ncard.choose 2) ((Fintype.card ↑A.verts).choose 2) (eq_of_heq ((fun a a' e'_1 a_1 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_1 ≍ x → a.choose a_1 ≍ a'.choose a_1) e'_1 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_1 : a = a'), e_1 ≍ Eq.refl a → a.choose a_1 ≍ a'.choose a_1) (fun e_1 h => HEq.refl (a.choose a_1)) (Eq.symm h) e'_1) (Eq.refl a') (HEq.refl e'_1)) A.verts.ncard (Fintype.card ↑A.verts) (Eq.mpr (id (congrArg (fun _a => _a = Fintype.card ↑A.verts) (Set.ncard_eq_toFinset_card A.verts h_fin))) (Eq.mpr (id (congrArg (fun _a => _a = Fintype.card ↑A.verts) (Set.Finite.card_toFinset h_fin))) (Eq.refl (Fintype.card ↑A.verts)))) 2)))) card_edgeFinset_le_card_choose_two)⊢ A.edgeSet ⊆ A.edgeSet All goals completed! 🐙, ?_, rfl⟩ V:Type uG:SimpleGraph Vn:ℕm:ℕA:G.Subgraphhn:A.verts.ncard = nh_fin:A.verts.Finiteh:sInf {x | ∃ E, ∃ (_ : E ⊆ A.edgeSet) (_ : (A.deleteEdges E).coe.IsBipartite), E.ncard = x} = mthis:A.edgeSet.ncard ≤ n.choose 2 := Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard ≤ _a.choose 2) (Eq.symm hn))) (have this := h_fin.fintype; have this_1 := Fintype.ofFinite ↑A.coe.edgeSet; Eq.mpr (eq_of_heq ((fun α self a a' e'_3 a_1 a'_1 e'_4 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a'_1)) (fun e_3 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_4 ≍ x → (a ≤ a_1) ≍ (a ≤ a'_1)) e'_4 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_4 : a_1 = a'), e_4 ≍ Eq.refl a_1 → (a ≤ a_1) ≍ (a ≤ a')) (fun e_4 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_4) (Eq.refl a'_1) (HEq.refl e'_4)) (Eq.symm h) e'_3) (Eq.refl a') (HEq.refl e'_3)) ℕ instLENat A.edgeSet.ncard A.coe.edgeFinset.card (Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard = _a) (Eq.symm (Set.ncard_coe_finset A.coe.edgeFinset)))) (Eq.mpr (id (congrArg (fun _a => A.edgeSet.ncard = _a.ncard) (coe_edgeFinset A.coe))) (Eq.mpr (id (congrArg (fun _a => _a.ncard = A.coe.edgeSet.ncard) (Eq.symm (Subgraph.image_coe_edgeSet_coe A)))) ((Set.ncard_image_iff (Set.toFinite A.coe.edgeSet)).mpr (Function.Injective.injOn (Sym2.map.injective Subtype.coe_injective)))))) (A.verts.ncard.choose 2) ((Fintype.card ↑A.verts).choose 2) (eq_of_heq ((fun a a' e'_1 a_1 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_1 ≍ x → a.choose a_1 ≍ a'.choose a_1) e'_1 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_1 : a = a'), e_1 ≍ Eq.refl a → a.choose a_1 ≍ a'.choose a_1) (fun e_1 h => HEq.refl (a.choose a_1)) (Eq.symm h) e'_1) (Eq.refl a') (HEq.refl e'_1)) A.verts.ncard (Fintype.card ↑A.verts) (Eq.mpr (id (congrArg (fun _a => _a = Fintype.card ↑A.verts) (Set.ncard_eq_toFinset_card A.verts h_fin))) (Eq.mpr (id (congrArg (fun _a => _a = Fintype.card ↑A.verts) (Set.Finite.card_toFinset h_fin))) (Eq.refl (Fintype.card ↑A.verts)))) 2)))) card_edgeFinset_le_card_choose_two)⊢ ∀ {a b : ↑A.verts}, (A.deleteEdges A.edgeSet).coe.Adj a b → (completeGraph (Fin 2)).Adj 0 0 All goals completed! 🐙

For a given graph $G$ and size $n$, this defines the smallest number $k$ such that any subgraph of $G$ on $n$ vertices can be made bipartite by deleting at most $k$ edges.

This value is optimal because it is the maximum of minEdgeDistToBipartite taken over all $n$-vertex subgraphs. This means there exists at least one $n$-vertex subgraph that requires exactly this many edge deletions. This is Definition 3.1 in [EHS82].

[EHS82] Erdős, P. and Hajnal, A. and Szemerédi, E., On almost bipartite large chromatic graphs Theory and practice of combinatorics (1982), 117-123.

noncomputable def SimpleGraph.maxSubgraphEdgeDistToBipartite (G : SimpleGraph V) (n : ℕ) : ℕ := sSup <| SimpleGraph.subgraphEdgeDistsToBipartite G n

Let $f(n)\to \infty$ possibly very slowly. Is there a graph of infinite chromatic number such that every finite subgraph on $n$ vertices can be made bipartite by deleting at most $f(n)$ edges?

@[category research open, AMS 5] theorem declaration uses 'sorry'erdos_74 : answer(sorry) ↔ ∀ f : ℕ → ℕ, Tendsto f atTop atTop → (∃ (V : Type u) (G : SimpleGraph V), G.chromaticNumber = ⊤ ∧ ∀ n, G.maxSubgraphEdgeDistToBipartite n ≤ f n) := ⊢ True ↔ ∀ (f : ℕ → ℕ), Tendsto f atTop atTop → ∃ V G, χ(G) = ⊤ ∧ ∀ (n : ℕ), SimpleGraph.maxSubgraphEdgeDistToBipartite G n ≤ f n All goals completed! 🐙

Is there a graph of infinite chromatic number such that every finite subgraph on $n$ vertices can be made bipartite by deleting at most $\sqrt{n}$ edges?

@[category research open, AMS 5] theorem declaration uses 'sorry'erdos_74.variants.sqrt : answer(sorry) ↔ ∃ (V : Type u) (G : SimpleGraph V), G.chromaticNumber = ⊤ ∧ ∀ n, G.maxSubgraphEdgeDistToBipartite n ≤ (n : ℝ).sqrt := ⊢ True ↔ ∃ V G, χ(G) = ⊤ ∧ ∀ (n : ℕ), ↑(SimpleGraph.maxSubgraphEdgeDistToBipartite G n) ≤ √↑n All goals completed! 🐙 -- TODO(firsching): add the remaining statements/comments end Erdos74