/-
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 FormalConjecturesUtilErdős Problem 184
[BM22] Bucić, M. and Montgomery, R., Towards the Erdős-Gallai Cycle Decomposition Conjecture. arXiv:2211.07689 (2022).
[CFS14] Conlon, David and Fox, Jacob and Sudakov, Benny, Cycle packing. Random Structures Algorithms (2014), 608-626.
[EGP66] Erdős, Paul and Goodman, A. W. and Pósa, Lajos, The representation of a graph by set intersections. Canadian J. Math. (1966), 106-112.
[Er71] Erdős, P., Some unsolved problems in graph theory and combinatorial analysis. Combinatorial Mathematics and its Applications (Proc. Conf., Oxford, 1969) (1971), 97-109.
open Filter SimpleGraph Classical
namespace Erdos184
A graph $H$ is a cycle or an edge if it is connected and 2-regular, or if it has exactly one edge.
def IsCycleOrEdge {U : Type*} [Fintype U] (H : SimpleGraph U) : Prop :=
(H.Connected ∧ H.IsRegularOfDegree 2) ∨ H.edgeFinset.card = 1D is a decomposition of G into subgraphs.
def IsDecomposition {V : Type*} (G : SimpleGraph V) (D : Finset G.Subgraph) : Prop :=
Set.PairwiseDisjoint (D : Set G.Subgraph) (fun H ↦ H.edgeSet) ∧
(⋃ H ∈ D, H.edgeSet) = G.edgeSet
Any graph on $n$ vertices can be decomposed into $O(n)$ many edge-disjoint cycles and edges.
@[category research open, AMS 5]
theorem erdos_184 :
∃ f : ℕ → ℝ,
(f =O[atTop] fun n : ℕ ↦ (n : ℝ)) ∧
∀ {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V),
∃ (D : Finset G.Subgraph),
(∀ H ∈ D, IsCycleOrEdge H.coe) ∧
IsDecomposition G D ∧
(D.card : ℝ) ≤ f (Fintype.card V) := ⊢ ∃ f,
(f =O[atTop] fun n => ↑n) ∧
∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V),
∃ D, (∀ H ∈ D, IsCycleOrEdge H.coe) ∧ IsDecomposition G D ∧ ↑D.card ≤ f (Fintype.card V)
All goals completed! 🐙
Erdős and Gallai [EGP66] proved that $O(n \log n)$ many cycles and edges suffices.
@[category research solved, AMS 5]
theorem erdos_184.variants.n_log_n :
∃ f : ℕ → ℝ,
(f =O[atTop] fun n : ℕ ↦ (n : ℝ) * Real.log (n : ℝ)) ∧
∀ {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V),
∃ (D : Finset G.Subgraph),
(∀ H ∈ D, IsCycleOrEdge H.coe) ∧
IsDecomposition G D ∧
(D.card : ℝ) ≤ f (Fintype.card V) := ⊢ ∃ f,
(f =O[atTop] fun n => ↑n * Real.log ↑n) ∧
∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V),
∃ D, (∀ H ∈ D, IsCycleOrEdge H.coe) ∧ IsDecomposition G D ∧ ↑D.card ≤ f (Fintype.card V)
All goals completed! 🐙
The graph $K_{3,n-3}$ shows that at least $(1+c)n$ many cycles and edges are required, for some constant $c>0$.
@[category research solved, AMS 5]
theorem erdos_184.variants.lower_bound :
∃ c > 0, ∀ᶠ n in atTop,
let G : SimpleGraph (Fin n) := fromRel (fun (i j : Fin n) => (i : ℕ) < 3 ∧ 3 ≤ (j : ℕ));
∀ (D : Finset G.Subgraph),
(∀ H ∈ D, IsCycleOrEdge H.coe) →
IsDecomposition G D →
(1 + c) * (n : ℝ) ≤ (D.card : ℝ) := ⊢ ∃ c > 0,
∀ᶠ (n : ℕ) in atTop,
let G := fromRel fun i j => ↑i < 3 ∧ 3 ≤ ↑j;
∀ (D : Finset G.Subgraph), (∀ H ∈ D, IsCycleOrEdge H.coe) → IsDecomposition G D → (1 + c) * ↑n ≤ ↑D.card
All goals completed! 🐙
In [Er71] Erdős suggests that only $n-1$ many cycles and edges are required if we do not require them to be edge-disjoint.
@[category research open, AMS 5]
theorem erdos_184.variants.covering :
answer(sorry) ↔
∀ {V : Type} [Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V),
∃ (D : Finset G.Subgraph),
(∀ H ∈ D, IsCycleOrEdge H.coe) ∧
(⋃ H ∈ D, H.edgeSet) = G.edgeSet ∧
(D.card : ℝ) ≤ (Fintype.card V : ℝ) - 1 := ⊢ True ↔
∀ {V : Type} [inst : Fintype V] [DecidableEq V] [Nonempty V] (G : SimpleGraph V),
∃ D, (∀ H ∈ D, IsCycleOrEdge H.coe) ∧ ⋃ H ∈ D, H.edgeSet = G.edgeSet ∧ ↑D.card ≤ ↑(Fintype.card V) - 1
All goals completed! 🐙
The best bound available is due to Bucić and Montgomery [BM22], who prove that $O(n\log^* n)$ many cycles and edges suffice, where $\log^*$ is the iterated logarithm function.
@[category research solved, AMS 5]
theorem erdos_184.variants.bucic_montgomery :
∃ f : ℕ → ℝ,
(f =O[atTop] fun n : ℕ ↦ (n : ℝ) * (Real.iteratedLog (n : ℝ) : ℝ)) ∧
∀ {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V),
∃ (D : Finset G.Subgraph),
(∀ H ∈ D, IsCycleOrEdge H.coe) ∧
IsDecomposition G D ∧
(D.card : ℝ) ≤ f (Fintype.card V) := ⊢ ∃ f,
(f =O[atTop] fun n => ↑n * ↑(↑n).iteratedLog) ∧
∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V),
∃ D, (∀ H ∈ D, IsCycleOrEdge H.coe) ∧ IsDecomposition G D ∧ ↑D.card ≤ f (Fintype.card V)
All goals completed! 🐙
Conlon, Fox, and Sudakov [CFS14] proved that $O_\epsilon(n)$ cycles and edges suffice if $G$ has minimum degree at least $\epsilon n$, for any $\epsilon>0$.
@[category research solved, AMS 5]
theorem erdos_184.variants.conlon_fox_sudakov :
∀ ε > 0, ∃ f : ℕ → ℝ,
(f =O[atTop] fun n : ℕ ↦ (n : ℝ)) ∧
∀ {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V),
(G.minDegree : ℝ) ≥ ε * (Fintype.card V : ℝ) →
∃ (D : Finset G.Subgraph),
(∀ H ∈ D, IsCycleOrEdge H.coe) ∧
IsDecomposition G D ∧
(D.card : ℝ) ≤ f (Fintype.card V) := ⊢ ∀ ε > 0,
∃ f,
(f =O[atTop] fun n => ↑n) ∧
∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V),
↑G.minDegree ≥ ε * ↑(Fintype.card V) →
∃ D, (∀ H ∈ D, IsCycleOrEdge H.coe) ∧ IsDecomposition G D ∧ ↑D.card ≤ f (Fintype.card V)
All goals completed! 🐙
end Erdos184