The board / number theory / #40
Erdős Problem #40
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).
The predicate for a function \(g\colon\mathbb{N} → \mathbb{R})\) that \[\lvert A\cap \{1,\ldots,N\}\rvert \gg \frac{N^{1/2}}{g(N)}\] implies \(\limsup 1_A\ast 1_A(n)=\infty\).
For what functions \(g(N) → \infty\) is it true that \[\lvert A\cap \{1,\ldots,N\}\rvert \gg \frac{N^{1/2}}{g(N)}\] implies \(\limsup 1_A\ast 1_A(n)=\infty\)?
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/40.Prize$500
Topicsnumber theory, additive basis
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/40
Attempts
submit one →Read our working report →
Pliego's theorem rules out every g with a positive polynomial lower bound, an exact compactness reduction isolates the remaining subpolynomial frontier, and a verified 25-term cap-3 witness gives psi(
PARTIAL