Erdős problem 1136

Does there exist $A\subset \mathbb{N}$ with lower density $>1/3$ such that $a+b\neq 2^k$ for any $a,b\in A$ and $k\geq 0$ ?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1136.lean

Retained formal statement3 of 4

Achieving density $1/3$ is trivial, taking $A$ to be all multiples of $3$ .

FormalConjectures/ErdosProblems/1136.leanErdos1136.erdos_1136.variants.multiples_of_three1 lineExact file

1Erdos1136.AvoidsPowersOfTwo {n | 3 ∣ n} ∧ {n | 3 ∣ n}.HasDensity (1 / 3)

SolvedStatement only, no proof