Erdős problem 184

Any graph on $n$ vertices can be decomposed into $O(n)$ many edge-disjoint cycles and edges.

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

184.lean

Retained formal statement2 of 6

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.

FormalConjectures/ErdosProblems/184.leanErdos184.erdos_184.variants.bucic_montgomery4 linesExact file

1∃ f,2  (f =O[Filter.atTop] fun n => ↑n * ↑(↑n).iteratedLog) ∧3    ∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V),4      ∃ D, (∀ H ∈ D, Erdos184.IsCycleOrEdge H.coe) ∧ Erdos184.IsDecomposition G D ∧ ↑D.card ≤ f (Fintype.card V)

SolvedStatement only, no proof

Source providers

Erdős Problems1
locator only
Formal Conjectures6
statement retained
VibeMathed0
not observed here
PLBY Lean proofs0
not observed here
Jayyhk Erdős Lean0
not observed here
William Blair Lean proofs0
not observed here
Erdős AI contributions wiki0
not observed here
GPT-Erdős0
not observed here

Referenced paths

FormalConjectures/
- ErdosProblems/
  - 184.lean6