Skip to content

Erdős problem 153

Start work

Let AA be a finite Sidon set and A+A={s1<⋯<st}A+A=\{s_1<\cdots<s_t\}. Is it true that 1t∑1≤i<t(si+1−si)2→∞\frac{1}{t}\sum_{1\leq i<t}(s_{i+1}-s_i)^2 \to \infty as ∣A∣→∞\lvert A\rvert\to \infty?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

153.lean

Retained formal statement1 of 1

Let AA be a finite Sidon set and A+A={s1<⋯<st}A+A=\{s_1<\cdots<s_t\}. Is it true that 1t∑1≤i<t(si+1−si)2→∞\frac{1}{t}\sum_{1\leq i<t}(s_{i+1}-s_i)^2 \to \infty as ∣A∣→∞\lvert A\rvert\to \infty?

FormalConjectures/ErdosProblems/153.leanErdos153.erdos_1531 lineExact file
True ↔ Filter.Tendsto Erdos153.f Filter.atTop Filter.atTop
OpenStatement only, no proof