Skip to content

Erdős problem 45

Let k2k\geq 2. Is there an integer nkn_k such that, if D={1<d<nk:dnk}D=\{ 1<d<n_k : d\mid n_k\}, then for any kk-colouring of DD there is a monochromatic subset DDD'\subseteq D such that dD1d=1\sum_{d\in D'}\frac{1}{d}=1?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

45.lean

Retained formal statement1 of 1

Let k2k\geq 2. Is there an integer nkn_k such that, if D={1<d<nk:dnk}D=\{ 1<d<n_k : d\mid n_k\}, then for any kk-colouring of DD there is a monochromatic subset DDD'\subseteq D such that dD1d=1\sum_{d\in D'}\frac{1}{d}=1?

This follows from the colouring result of Croot [Cr03]. Croot's result allows for nkeCkn_k \leq e^{C^k} for some constant C>1C>1 (simply taking nkn_k to be the lowest common multiple of some interval [1,Ck][1,C^k]). Sawhney has observed that there is also a doubly exponential lower bound, and hence this bound is essentially sharp.

FormalConjectures/ErdosProblems/45.leanErdos45.erdos_456 linesExact file
True  ∀ (k : ℕ),    2 ≤ kn,        ∀ (colouring : ℕ → Fin k),colour, ∃ D' ⊆ {dn.divisors | 1 < dd < n}, (∀ dD', colouring d = colour) ∧ D'.reciprocalSum = 1
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Search problems.science

Find a Problem, Result, source, or page