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 statement4 of 4

Müller also proved this is best possible, in that $A$ with the property in the question has lower density at most $1/2$ .

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

1∀ (A : Set ℕ), Erdos1136.AvoidsPowersOfTwo A → A.lowerDensity ≤ 1 / 2

SolvedStatement only, no proof