Erdős Problem #864

The question

Let $A\subseteq \{1,\dots ,N\}$ be a set such that there exists at most one $n$ with more than one solution to $n=a+b$ (with $a\le b\in A$). Estimate the maximal possible size of $|A|$. In particular, is it true that $$|A|\le (1+o(1))\frac{2}{\sqrt{3}}{N}^{1/2}?$$

A problem of Erdős and Freud [ErFr91] [Er92c]. For the analogous question with $n=a-b$ they prove that $|A|\sim N^{1/2}$. This is a weaker form of Erdős Problem 840.

The condition on $A$ is HasAtMostOneRepeatedSum. We state the question as follows: for every $\epsilon >0$ and all large $N$, every such set $A$ satisfies $|A|\le (1+\epsilon )\frac{2}{\sqrt{3}}{N}^{1/2}$.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.ErdosProblems.«864».

theorem erdos_864 :
    ∀ ε : ℝ, 0 < ε → ∀ᶠ N : ℕ in atTop, ∀ A ⊆ Finset.Icc 1 N,
      HasAtMostOneRepeatedSum A →
        (#A : ℝ) ≤ (1 + ε) * (2 / Real.sqrt 3) * Real.sqrt (N : ℝ)

What counts as progress

• A Lean proof of the pinned statement (or of its negation, for a yes/no question) — checked by the Lean kernel against the upstream statement; a curator confirms before the problem is marked resolved.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already — check erdosproblems.com/864. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• erdosproblems.com/864
• A389182
• [ErFr91] Erdős, P. and Freud, R., On sums of a Sidon-sequence. J. Number Theory 38 (1991), 196--205.
• [Er92c] Erdős, P., Some of my forgotten problems in number theory. Hardy-Ramanujan J. 15 (1992), 34-50.

Source and licence

Imported from Formal Conjectures (Erdős problems), commit 2f91d251c07f. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.