Source labels openChecked July 26, 2026

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$ ?

Combinatorics AMS 5

Mathematical statement

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?

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_566

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem erdos_566 : answer(sorry) ↔    ∀ (p : ℕ) (G : SimpleGraph (Fin p)),      -- G is sparse: every induced subgraph on k ≥ 2 vertices has ≤ 2k - 3 edges      (∀ S : Finset (Fin p), 2 ≤ S.card → (G.induce S).edgeSet.ncard ≤ 2 * S.card - 3) →      -- Then G is Ramsey size linear      ∃ c > (0 : ℝ), ∀ (n : ℕ) (H : SimpleGraph (Fin n)) [DecidableRel H.Adj],        -- H has no isolated vertices        (∀ v, 0 < H.degree v) →        -- r̂(G,H) ≤ c · m        (sizeRamsey G H : ℝ) ≤ c * H.edgeSet.ncard := 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

Pinned Formal Conjectures sourceformalization erdosproblems.com/566background