ErdosProblems · research open · AMS 5
unsolvedsorry — nobody on it
Erdős Problem 563
Conjecture 563 · Erdős
Let denote the smallest such that there exists a -colouring of the edges of so that every with contains more than many edges of each colour.
Prove that, for every , for some constant depending only on .
This problem is #39 in Ramsey Theory in the graphs problem collection.
Formal statement · Lean 4.lean
theorem erdos_563 :
∀ (α : ℝ), 0 ≤ α → α < 1 / 2 →
∃ (c : ℝ), 0 < c ∧
Tendsto (fun n : ℕ => (F n α : ℝ) / Real.log n) atTop (nhds c) := by
sorryProof. sorry
Nobody has tried yet.