Upper bounds for Sidon sets

DefinitionLargest Sidon subset of \(\{1, \dots, N\}\) (Green's Problem 31)#✓fully proved

For a natural number \(N\), \(F(N)\) is the largest cardinality of a Sidon subset of \([N] = \{1, \dots, N\}\).

noncomputable def maxSidonSubsetSize (N : ℕ) : ℕ :=
  sSup {k | ∃ A : Finset ℕ, A ⊆ Finset.Icc 1 N ∧ (A : Set ℕ).IsSidon ∧ A.card = k}

Uses 1 · Used by 1

Statement usesSidon set

Used byGreen's Problem 31: improving Lindström's upper bound

DefinitionGreen's Problem 31: improving Lindström's upper bound#✓fully proved

Let \(F(N)\) be the largest size of a Sidon subset of \(\{1, \dots, N\}\). The statement is that there are a real constant \(c < 1\) and a natural number \(N_0\) such that \(F(N) \le \sqrt{N} + c N^{1/4}\) for all \(N \ge N_0\).

Lindström's bound is \(F(N) \le N^{1/2} + N^{1/4} + O(1)\); the statement asks for a constant below \(1\) in the second term.

def sidonUpperBoundImproved : Prop :=
  ∃ c : ℝ, c < 1 ∧ ∃ N₀ : ℕ, ∀ N, N₀ ≤ N →
    (maxSidonSubsetSize N : ℝ) ≤ Real.sqrt N + c * (N : ℝ) ^ ((1 : ℝ) / 4)

noncomputable def maxSidonSubsetSize (N : ℕ) : ℕ :=
  sSup {k | ∃ A : Finset ℕ, A ⊆ Finset.Icc 1 N ∧ (A : Set ℕ).IsSidon ∧ A.card = k}

WantedExt/Combinatorics/SidonUpperBoundImprovementGreenProblem31Wanted.lean:40

Uses 1 · Used by 1

Statement usesLargest Sidon subset of \(\{1, \dots, N\}\) (Green's Problem 31)

Used byLindström's upper bound for Sidon sets can be improved

TheoremLindström's upper bound for Sidon sets can be improved#●ready to prove

Let \(F(N)\) be the largest size of a Sidon subset of \(\{1, \dots, N\}\). There are a real constant \(c < 1\) and a natural number \(N_0\) such that \(F(N) \le \sqrt{N} + c N^{1/4}\) for all \(N \ge N_0\).

Balogh, Füredi and Roy proved this with \(c = 0.998\); Carter, Hunter and O'Bryant later lowered the constant to \(0.98183\).

public theorem_wanted sidonUpperBoundImproved_holds : sidonUpperBoundImproved

def sidonUpperBoundImproved : Prop :=
  ∃ c : ℝ, c < 1 ∧ ∃ N₀ : ℕ, ∀ N, N₀ ≤ N →
    (maxSidonSubsetSize N : ℝ) ≤ Real.sqrt N + c * (N : ℝ) ^ ((1 : ℝ) / 4)

WantedExt/Combinatorics/SidonUpperBoundImprovementGreenProblem31Wanted.lean:45

Sources

B. Green, 100 open problems, Problem 31 (manuscript, update of December 2025), https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf; resolution: J. Balogh, Z. Füredi and S. Roy, An upper bound on the size of Sidon sets, Amer. Math. Monthly 130 (2023), 437-445, doi:10.1080/00029890.2023.2176667; arXiv:2103.15850, abstract: the maximum size of a Sidon set of {1, ..., n} is at most √n + 0.998 n^{1/4} for sufficiently large n; Green, Problem 31, 'Update 2021' records this bound and its 2023 improvement to 0.98183 (D. Carter, Z. Hunter and K. O'Bryant, Acta Math. Hungar. 175 (2025), 108-126), https://doi.org/10.1080/00029890.2023.2176667.

Uses 1

Statement usesGreen's Problem 31: improving Lindström's upper bound

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.