Erdős Problem 184: Covering
In [Er71] Erdős suggests that only many cycles and edges are required if we do not require them to be edge-disjoint.
Mathematical statement
In [Er71] Erdős suggests that only many cycles and edges are required if we do not require them to be edge-disjoint.
Statement source: Erdős Problems statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
erdos_184.variants.covering
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 := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References