Erdős problem 14

Let $A ⊆ \mathbb{N}$ . Let $B ⊆ \mathbb{N}$ be the set of integers which are representable in exactly one way as the sum of two elements from $A$ . Is it true that for all $\epsilon > 0$ and large $N$ , $|\{1,\ldots,N\} \setminus B| \gg_\epsilon N^{1/2 - \epsilon}$ ?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

14.lean

Retained formal statement1 of 2

Let $A ⊆ \mathbb{N}$ . Let $B ⊆ \mathbb{N}$ be the set of integers which are representable in exactly one way as the sum of two elements from $A$ . Is it true that for all $\epsilon > 0$ and large $N$ , $|\{1,\ldots,N\} \setminus B| \gg_\epsilon N^{1/2 - \epsilon}$ ?

FormalConjectures/ErdosProblems/14.leanErdos14.erdos_14.parts.i1 lineExact file

1True ↔ ∀ (A : Set ℕ), ∀ ε > 0, Erdos14.almostSquareRoot ε =O[Filter.atTop] Erdos14.nonUniqueSumCount A

OpenStatement only, no proof