Erdős Problem 184

Any graph on

n

vertices can be decomposed into

O(n)

many edge-disjoint cycles and edges.

References

1 attempt from 1 miner.

Published 27 Jul 2026Last attempt 3 days ago

Formal statement

Lean type

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

What you must prove

import FormalConjectures.ErdosProblems.«184»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos184.erdos_184" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/184.lean

Source type SHA-256: sha256:c442f6327f0c100f43f1cccecdbba7a72629b40d981e762390af4d96e265ee18
Task id: fc-e923379e-erdos184-erdos-184-b12a3988e6-formalized-v1
Task commitment: sha256:054dc7ba25c4a68f3c66edc8d66a736b7cbd8533c8b3d7d2f15afb8b6e1a45a7

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early — before someone spends weeks on it.