Erdős Problem 329: Maximum Density of Sidon Sets

References:

• erdosproblems.com/329
• [AlMi25] B. Alexeev and D. G. Mixon, Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof. arXiv:2510.19804 (2025).
• [Ha47] Hall, Jr., Marshall, Cyclic projective planes. Duke Math. J. (1947), 1079--1090.

noncomputable def Erdos329.sqrtPartialDensity (A : Set ℕ) (N : ℕ) : ℝ

The partial density of a Sidon set A up to N, normalized by dividing by √N instead of N. This measures how close the set comes to the optimal density for Sidon sets.

Equations

• Erdos329.sqrtPartialDensity A N = ↑(A ∩ Set.Icc 1 N).ncard / √↑N

noncomputable def Erdos329.sidonUpperDensity (A : Set ℕ) : ℝ

The upper density of a Sidon set A, normalized by √N.

Equations

• Erdos329.sidonUpperDensity A = Filter.limsup (fun (N : ℕ) => Erdos329.sqrtPartialDensity A N) Filter.atTop

theorem Erdos329.erdos_329 : sSup {x : ℝ | ∃ (A : Set ℕ) (_ : IsSidon A), sidonUpperDensity A = x} = sorry

Erdős Problem 329. Let A ⊆ ℕ be a Sidon set. How large can lim sup_{N → ∞} |A ∩ {1,…,N}| / N^{1/2} be?

theorem Erdos329.erdos_329.variants.lower_bound : ∃ (A : Set ℕ), IsSidon A ∧ sidonUpperDensity A ≥ 1 / 2

Erdős proved that upper density 1 / 2 can be attained; in particular, there exists a Sidon set whose upper density is at least 1 / 2.

theorem Erdos329.erdos_329.variants.kruckeberg_1961 : ∃ (A : Set ℕ), IsSidon A ∧ sidonUpperDensity A = 1 / √2

Krückeberg ([Kr61]) exhibited an infinite Sidon set A with sidonUpperDensity A = 1 / Real.sqrt 2, improving Erdős’ earlier 1 / 2 lower bound.

[Kr61] Krückeberg, Fritz, $B\sb{2}$-Folgen und verwandte Zahlenfolgen. J. Reine Angew. Math. (1961), 53-60.

theorem Erdos329.erdos_329.variants.turan_1941 (A : Set ℕ) : IsSidon A → sidonUpperDensity A ≤ 1

Erdős and Turán [ErTu41] proved the upper bound of 1.

[ErTu41] Erdős, P. and Turán, P., On a problem of Sidon in additive number theory, and on some related problems. J. London Math. Soc. (1941), 212-215.

theorem Erdos329.erdos_329.variants.converse_implication : sSup {x : ℝ | ∃ (A : Set ℕ) (_ : IsSidon A), sidonUpperDensity A = x} = 1 → ∀ (A : Finset ℕ), IsSidon ↑A → ∃ (D : Set ℕ) (n : ℕ) (_ : n > 0), ↑A ⊆ D ∧ IsPerfectDifferenceSet D n

The converse: if the maximum density is 1, then any finite Sidon set can be embedded in a perfect difference set modulo $n > 0$.

Since the consequent is false (due to the counterexamples in [Ha47] and [AlMi25]), this implication is logically equivalent to the statement that the maximum upper density of Sidon sets is NOT 1. Because the maximum upper density problem is still open, the truth value of this implication is also an open research problem.

theorem Erdos329.exists_sidon_pos_density : ∃ (A : Set ℕ), IsSidon A ∧ 0 < sidonUpperDensity A

It is possible to construct a Sidon set with positive density.