Conjectures.io

Combinatorics

Erdős 153

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?

References

  • [ESS94] Erdős, P. and Sárközy, A. and Sós, T., On Sum Sets of Sidon Sets, I. Journal of Number Theory (1994), 329-347.

No one has attempted this yet.

Formal statement

Lean type

True ↔ Filter.Tendsto Erdos153.f Filter.atTop Filter.atTop

What you must prove

import FormalConjectures.ErdosProblems.«153»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos153.erdos_153" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/153.lean

Source type SHA-256
sha256:b35a9b51e1956e50dac187c15f5e0fd861c1ae3dcaaceb7941a1ce9bfd770316
Task id
fc-379fc029-erdos153-erdos-153-1613e703d8-formalized-v1
Task commitment
sha256:9cd064c1d83d506252dd731c9ad84067c283db90b343cfb6f7566c0e0c6ff51b

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.