Skip to content

Erdős problem 45

Let k≥2k\geq 2. Is there an integer nkn_k such that, if D={1<d<nk:d∣nk}D=\{ 1<d<n_k : d\mid n_k\}, then for any kk-colouring of DD there is a monochromatic subset D′⊆DD'\subseteq D such that ∑d∈D′1d=1\sum_{d\in D'}\frac{1}{d}=1?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

45.lean

Retained formal statement1 of 1

Let k≥2k\geq 2. Is there an integer nkn_k such that, if D={1<d<nk:d∣nk}D=\{ 1<d<n_k : d\mid n_k\}, then for any kk-colouring of DD there is a monochromatic subset D′⊆DD'\subseteq D such that ∑d∈D′1d=1\sum_{d\in D'}\frac{1}{d}=1?

This follows from the colouring result of Croot [Cr03]. Croot's result allows for nk≤eCkn_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 ≤ k →      ∃ n,        ∀ (colouring : ℕ → Fin k),          ∃ colour, ∃ D' ⊆ {d ∈ n.divisors | 1 < d ∧ d < n}, (∀ d ∈ D', 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.