Sidon sets

DefinitionSidon set#✓fully proved

A set in an additive commutative monoid is Sidon when every equality of two pairwise sums is trivial up to swapping the summands. Repeated summands are included.

def IsSidon {α : Type*} [AddCommMonoid α] (A : Set α) : Prop :=
  ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A,
    a + b = c + d → (a = c ∧ b = d) ∨ (a = d ∧ b = c)

Used by 16

Used byGolomb ruler lengths · Sidon subsets of \(\{1, \dots, N\}\) · Mian–Chowla lower bound for an infinite Sidon set · Ajtai–Komlós–Szemerédi lower bound for an infinite Sidon set · Ruzsa's lower bound for an infinite Sidon set · A Sidon set outside the almost thin ideal · Weak Sidon sets split into two Sidon sets · Positive sets whose elements at least double are Sidon · Sidon sets are weak Sidon sets · A block not covered by few Sidon sets · Sidon ideal · Erdős Problem 707, weak form · Erdős Problem 707 · Erdős Problem 198 · Finite Sidon sets of natural numbers · Largest Sidon subset of \(\{1, \dots, N\}\) (Green's Problem 31)

DefinitionFinite Sidon sets of natural numbers#✓fully proved

A finite set \(A\) of natural numbers is a Sidon set when every equality \(a + b = c + d\) with \(a, b, c, d \in A\) is trivial, that is, \(a = c\) and \(b = d\), or \(a = d\) and \(b = c\).

def IsSidon (A : Finset ℕ) : Prop :=
  Set.IsSidon (A : Set ℕ)

Uses 1 · Used by 1

Statement usesSidon set

Used byErdős Problem 152 on isolated sums of Sidon sets

DefinitionSumset of a finite set of natural numbers#✓fully proved

For a finite set \(A\) of natural numbers, the sumset \(A + A\) is the finite set of all sums \(x + y\) with \(x, y \in A\).

def Sumset (A : Finset ℕ) : Finset ℕ :=
  (A.product A).image (fun p => p.1 + p.2)

Used by 1

Used byErdős Problem 152 on isolated sums of Sidon sets

DefinitionIsolated elements of a set of natural numbers#✓fully proved

Let \(S\) be a finite set of natural numbers. A natural number \(a\) is isolated in \(S\) when \(a \in S\), \(a + 1 \notin S\), and either \(a = 0\) or \(a - 1 \notin S\).

For \(a = 0\) the condition on the predecessor is vacuous, since \(0\) has no predecessor among the natural numbers.

def IsIsolated (S : Finset ℕ) (a : ℕ) : Prop :=
  a ∈ S ∧ a + 1 ∉ S ∧ (a = 0 ∨ a - 1 ∉ S)

DefinitionNumber of isolated elements#✓fully proved

For a finite set \(S\) of natural numbers, the isolated count of \(S\) is the number of elements \(a \in S\) with \(a + 1 \notin S\) and either \(a = 0\) or \(a - 1 \notin S\).

def IsolatedCount (S : Finset ℕ) : ℕ :=
  (S.filter (fun a => a + 1 ∉ S ∧ (a = 0 ∨ a - 1 ∉ S))).card

Used by 1

Used byErdős Problem 152 on isolated sums of Sidon sets

DefinitionErdős Problem 152 on isolated sums of Sidon sets#✓fully proved

A finite set \(A\) of natural numbers is a Sidon set when \(a + b = c + d\) with \(a, b, c, d \in A\) implies \(\{a, b\} = \{c, d\}\), and its sumset is \(A + A = \{x + y : x, y \in A\}\). An element \(s\) of a finite set \(S\) of natural numbers is isolated in \(S\) when \(s + 1 \notin S\) and either \(s = 0\) or \(s - 1 \notin S\). The proposition asserts that for every natural number \(M \ge 1\) there is a natural number \(K\) such that every finite Sidon set \(A\) of natural numbers with at least \(K\) elements has at least \(M\) isolated elements in \(A + A\).

def conjecture : Prop :=
  ∀ M : ℕ, 1 ≤ M →
    ∃ K : ℕ, ∀ A : Finset ℕ,
      IsSidon A → K ≤ A.card → M ≤ IsolatedCount (Sumset A)

Uses 3 · Used by 1

Statement usesFinite Sidon sets of natural numbers · Number of isolated elements · Sumset of a finite set of natural numbers

Used byLarge Sidon sets have many isolated sums

TheoremLarge Sidon sets have many isolated sums#●ready to prove

For every natural number \(M \ge 1\) there is a natural number \(K\) such that every finite Sidon set \(A\) of natural numbers with at least \(K\) elements has at least \(M\) isolated elements in its sumset \(A + A = \{x + y : x, y \in A\}\). Here \(A\) is a Sidon set when \(a + b = c + d\) with \(a, b, c, d \in A\) implies \(\{a, b\} = \{c, d\}\), and an element \(s\) of \(A + A\) is isolated when \(s + 1 \notin A + A\) and either \(s = 0\) or \(s - 1 \notin A + A\).

This answers Erdős Problem 152 affirmatively: Tsoukalas et al. show, with a Lean proof, that every Sidon set \(A\) of \(n\) natural numbers has at least \((n^2 - 100n - 16)/16\) isolated elements in \(A + A\).

public theorem_wanted conjecture_holds : conjecture

Sources

• George Tsoukalas et al., Advancing Mathematics Research with AI-Driven Formal Proof Search, arXiv preprint (2026), arXiv:2605.22763, https://arxiv.org/abs/2605.22763.

Uses 1

Statement usesErdős Problem 152 on isolated sums of Sidon sets

6 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.