feat(GreensOpenProblems): 2

[jeangud]

Description

Let $A \subset \mathbf{Z}$ be a set of $n$ integers. Is there a set $S \subset A$ of size $(\log n)^{100}$ such that the restricted sumset $S \hat{+} S$ is disjoint from $A$?

The restricted sumset of a set $S$, denoted $S \hat{+} S$, is the set $\lbrace s_1 + s_2 : s_1, s_2 \in S, s_1 \neq s_2 \rbrace$.

• Closes Green's Open Problems #2 #890
• Added some proven bounds as additional variants

Testing

✅ Builds successfully.

$ lake build FormalConjectures/GreensOpenProblems/2.lean 
Build completed successfully.

[mo271]

Thanks!

Main statement is buggy, see the prove of its negation

[YaelDillies]

Thanks!