Combinatorics
A ⊆ {1,…,N} be a Sidon set. Is it true that, for any ε > 0,
there exist M = M(ε) and B ⊆ {N+1,…,M} such that A ∪ B ⊆ {1,…,M} is a Sidon set
of size at least (1−ε)M^{1/2}?
This problem asks whether any Sidon set can be extended to achieve a density
arbitrarily close to the optimal density for Sidon sets.
$4,992 bounty1 piece from 1 personlast one last month
Nobody has attempted this. A complete proof or refutation takes the whole bounty.
A lemma, a definition, a special case. There is no race: when someone finishes the problem, the pool splits between everyone whose work led there.
contrib new erdos-44Command line, then a pull request on GitHub.
1 piece · 2 lemmas
1 Sept 2026
The textbook Sidon bound: maxSidonSubsetCard (Icc 1 N) is at most 2 sqrt N
5FqLp5…FfZZiK · 2 lemmas
Formal statement
Proof target
import FormalConjectures.ErdosProblems.«44»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos44.erdos_44" := by
sorry
end Bounty
Original conjecture (Lean type)
True ↔
∀ N ≥ 1,
∀ A ⊆ Finset.Icc 1 N,
IsSidon ↑A → ∀ ε > 0, ∃ M > N, ∃ B ⊆ Finset.Icc (N + 1) M, IsSidon (↑A ∪ ↑B) ∧ (1 - ε) * √↑M ≤ ↑(A ∪ B).cardOriginal conjecture source: FormalConjectures/ErdosProblems/44.lean
References
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.
Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.