Problems/Erdos-Ginzburg-Ziv Theorem

Erdos-Ginzburg-Ziv Theorem

Number TheorySOLVED
Year
1961
Difficulty
*****
Solved by
Paul Erdos, Abraham Ginzburg & Abraham Ziv (1961)

Statement

Among any 2n-1 integers, there exist n whose sum is divisible by n.

∀ a1,…,a2n−1∈Z,  ∃ S⊂[2n−1],  ∣S∣=n:∑i∈Sai≡0(modn)\forall\, a_1,\ldots,a_{2n-1} \in \mathbb{Z},\; \exists\, S \subset [2n-1],\; |S|=n : \sum_{i\in S} a_i \equiv 0 \pmod{n}

About this Problem

Launched the field of zero-sum theory. The bound 2n-1 is tight.

About the Lean 4 Prover

Lean 4 is a theorem prover and programming language. When a proof compiles in Lean, it is mathematically certain to be correct — the type checker verifies every logical step. This is the gold standard for formal verification.

Our platform uses fal.ai serverless compute to run Lean verification, and Gemini to generate proof strategies that are then formally checked. ShinkaEvolve provides the evolutionary backbone for automated mathematical discovery.

Mathematical Art

Generate a unique AI illustration of this problem using fal.ai FLUX.

Connected Constellations

Number TheorySOLVED
Erdos-Kac Theorem
Number TheoryOPEN
Erdos-Straus Conjecture
Number TheoryOPEN
Erdos-Turan Conjecture on Additive Bases