Skip to content

Erdős problem 1136

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

Sources

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

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1136.lean

Retained formal statement1 of 4

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

Müller [Mu11] settled this question in the affirmative: in fact one can take AA to be the set of all integers congruent to 32i(mod2i+2)3\cdot 2^i\pmod{2^{i+2}} for any i0i\geq 0, which has density 1/21/2.

FormalConjectures/ErdosProblems/1136.leanErdos1136.erdos_11361 lineExact file
True ↔ ∃ A, 1 / 3 < A.lowerDensityErdos1136.AvoidsPowersOfTwo 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