Zero subset sums in cyclic groups

DefinitionThe Erdős–Heilbronn zero subset sum statement (Erdős Problem 540)#✓fully proved

This is the statement that there is a real number \(C > 0\) such that for every integer \(N \ge 1\), every set \(A \subseteq \mathbb{Z}/N\mathbb{Z}\) with \(|A| \ge C\sqrt{N}\) has a nonempty subset \(S \subseteq A\) whose elements sum to \(0\) in \(\mathbb{Z}/N\mathbb{Z}\).

def sqrtSizeHasZeroSubsetSum : Prop :=
  ∃ C : ℝ, 0 < C ∧ ∀ N : ℕ, 0 < N → ∀ A : Finset (ZMod N), C * Real.sqrt N ≤ A.card →
    ∃ S ⊆ A, S.Nonempty ∧ ∑ x ∈ S, x = 0

Used by 1

Used byZero subset sums of large sets in \(\mathbb{Z}/N\mathbb{Z}\) (Erdős Problem 540)

TheoremZero subset sums of large sets in \(\mathbb{Z}/N\mathbb{Z}\) (Erdős Problem 540)#●ready to prove

There is a real number \(C > 0\) such that for every integer \(N \ge 1\), every set \(A \subseteq \mathbb{Z}/N\mathbb{Z}\) with \(|A| \ge C\sqrt{N}\) has a nonempty subset \(S \subseteq A\) whose elements sum to \(0\) in \(\mathbb{Z}/N\mathbb{Z}\).

Resolved true: Olson proved it for prime \(N\) and Szemerédi for all \(N\) (in every finite abelian group); Hamidoune and Zémor showed \((1 + o(1))\sqrt{2N}\) suffices.

public theorem_wanted sqrtSizeHasZeroSubsetSum_holds : sqrtSizeHasZeroSubsetSum

Sources

• T. F. Bloom, Erdős Problems, Problem #540, https://www.erdosproblems.com/540 (status PROVED (LEAN)); resolution: E. Szemerédi, On a conjecture of Erdős and Heilbronn, Acta Arith. (1970), 227-229, erdosproblems.com/540: yes; Olson for N prime, Szemerédi for all N (indeed for all finite abelian groups), https://www.erdosproblems.com/540.

Uses 1

Statement usesThe Erdős–Heilbronn zero subset sum statement (Erdős Problem 540)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.