Skip to content

Erdős problem 221

Is there a set ANA\subset\mathbb{N} such that, for all large NN, A{1,,N}N/logN\lvert A\cap\{1,\ldots,N\}\rvert \ll N/\log N and such that every large integer can be written as 2k+a2^k+a for some k0k\geq 0 and aAa\in A?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

221.lean

Retained formal statement1 of 1

Is there a set ANA\subset\mathbb{N} such that, for all large NN, A{1,,N}N/logN\lvert A\cap\{1,\ldots,N\}\rvert \ll N/\log N and such that every large integer can be written as 2k+a2^k+a for some k0k\geq 0 and aAa\in A?

Lorentz [Lo54] proved there is such a set with, for all large NN, A{1,,N}loglogNlogNN\lvert A\cap\{1,\ldots,N\}\rvert \ll \frac{\log\log N}{\log N}N The answer is yes, proved by Ruzsa [Ru72].

FormalConjectures/ErdosProblems/221.leanErdos221.erdos_2214 linesExact file
TrueA,    ((fun N => ↑{a | aAaN}.ncard) =O[Filter.atTop] fun N => ↑N / Real.logN) ∧      ∀ᶠ (N : ℕ) in Filter.atTop, ∃ k a, 0 ≤ kaAN = 2 ^ k + a
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