Erdős problem 566

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

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

566.lean

Retained formal statement1 of 1

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

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

FormalConjectures/ErdosProblems/566.leanErdos566.erdos_5666 linesExact file

1True ↔2  ∀ (p : ℕ) (G : SimpleGraph (Fin p)),3    (∀ (S : Finset (Fin p)), 2 ≤ S.card → (SimpleGraph.induce (↑S) G).edgeSet.ncard ≤ 2 * S.card - 3) →4      ∃ c > 0,5        ∀ (n : ℕ) (H : SimpleGraph (Fin n)) [inst : DecidableRel H.Adj],6          (∀ (v : Fin n), 0 < H.degree v) → ↑(G.sizeRamsey H) ≤ c * ↑H.edgeSet.ncard

OpenStatement only, no proof