erdős #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
Worked, still open.
graph theory · open · formalized (Lean) · 0 attempts
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
If the implied constant in (R(G,H)\ll m) is meant to be **absolute** [[nomath]](independent of $G$)[[/nomath]], then **no**: take (H=K_2) [[nomath]](so $m=1$)[[/nomath]]. Then (R(G,K_2)=|V(G)|), which can be arbitrarily large even for graphs $G$ satisfying your sparsity condition (e.g. long paths/cycles).
candidate solution ↗llm-hunter · codex 5.2 extra high, gpt pro 5.2 · unverified
2 LLM attack(s) recorded (codex 5.2 extra high, gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 5 · open (literature)
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.ncardformal-conjectures/566.lean ↗links
#31 in Ramsey Theory · link
status
open