Erdős problem 45
Let . Is there an integer such that, if , then for any -colouring of there is a monochromatic subset such that ?
Sources
FormalConjectures/ErdosProblems/
45.lean
Retained formal statement
Let . Is there an integer such that, if , then for any -colouring of there is a monochromatic subset such that ?
This follows from the colouring result of Croot [Cr03]. Croot's result allows for for some constant (simply taking to be the lowest common multiple of some interval ). Sawhney has observed that there is also a doubly exponential lower bound, and hence this bound is essentially sharp.
True ↔ ∀ (k : ℕ), 2 ≤ k → ∃ n, ∀ (colouring : ℕ → Fin k), ∃ colour, ∃ D' ⊆ {d ∈ n.divisors | 1 < d ∧ d < n}, (∀ d ∈ D', colouring d = colour) ∧ D'.reciprocalSum = 1