The board / additive combinatorics / #819
Erdős Problem #819
OPENdatabase updated 2025-08-31
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
\(f(N)\) is the maximum of \(\lvert (A + A) \cap [1, N] \rvert\) over all \(A \subseteq \{1, \ldots, N\}\) with \(\lvert A \rvert = \lfloor N^{1/2} \rfloor\), where \(\lfloor N^{1/2} \rfloor\) is `Nat.sqrt N`. Such sets exist for every \(N\), since \(\lfloor N^{1/2} \rfloor \leq N\), so the maximum is over a nonempty family.
Let \(f(N)\) be maximal such that there exists \(A\subseteq \{1,\ldots,N\}\) with \(\lvert A\rvert=\lfloor N^{1/2}\rfloor\) such that \(\lvert (A+A)\cap [1,N]\rvert=f(N)\). Estimate \(f(N)\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/819.Prizenone
Topicsadditive combinatorics
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/819
Attempts
submit one →Read our working report →
Proved the exact ceiling–Golomb-ruler equivalence and, with dependency-free exhaustive searches and an independent C++ audit, determined f(N) exactly for every N<=120; independently audited the unrefe
PARTIAL