Skip to content

Erdős problem 1136

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

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1136.lean

Retained formal statement1 of 4

Does there exist A⊂NA\subset \mathbb{N} with lower density >1/3>1/3 such that a+b≠2ka+b\neq 2^k for any a,b∈Aa,b\in A and k≥0k\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 3⋅2i(mod2i+2)3\cdot 2^i\pmod{2^{i+2}} for any i≥0i\geq 0, which has density 1/21/2.

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