Erdős problem 566
Let be such that any subgraph on vertices has at most edges. Is it true that, if has edges and no isolated vertices, then ?
Sources
FormalConjectures/ErdosProblems/
566.lean
Retained formal statement
Let be such that any subgraph on vertices has at most edges. Is it true that, if has edges and no isolated vertices, then ?
In other words: if is sparse (every induced subgraph on vertices has edges), is Ramsey size linear?
True ↔ ∀ (p : ℕ) (G : SimpleGraph (Fin p)), (∀ (S : Finset (Fin p)), 2 ≤ S.card → (SimpleGraph.induce (↑S) G).edgeSet.ncard ≤ 2 * S.card - 3) → ∃ c > 0, ∀ (n : ℕ) (H : SimpleGraph (Fin n)) [inst : DecidableRel H.Adj], (∀ (v : Fin n), 0 < H.degree v) → ↑(G.sizeRamsey H) ≤ c * ↑H.edgeSet.ncardOpenStatement only, no proof