The board / number theory / #30
Erdős Problem #30
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).
Let \(h(N)\) be the maximum size of a Sidon set in \(\{1, \dots, N\}\).
Is it true that, for every \(\varepsilon > 0\), \(h(N) = \sqrt N + O_{\varepsilon}(N^\varepsilon)\)
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 8 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/30.Prize$1,000
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/30
Attempts
submit one →Read our working report →
The live page status is OPEN - $1000, but “Currently working on this problem” lists Emmanuel_Audigé_Y., Rynaldos, TerenceTao, and KMendoza (accessed 2026-07-26), so the mandatory no-collision rule app
SKIPPED