Skip to content

Erdős problem 566

Let GG be such that any subgraph on kk vertices has at most 2k32k-3 edges. Is it true that, if HH has mm edges and no isolated vertices, then r^(G,H)m\hat{r}(G,H) \ll m?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

566.lean

Retained formal statement1 of 1

Let GG be such that any subgraph on kk vertices has at most 2k32k-3 edges. Is it true that, if HH has mm edges and no isolated vertices, then r^(G,H)m\hat{r}(G,H) \ll m?

In other words: if GG is sparse (every induced subgraph on kk vertices has 2k3≤ 2k-3 edges), is GG Ramsey size linear?

FormalConjectures/ErdosProblems/566.leanErdos566.erdos_5666 linesExact file
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.ncard
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page