Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Olson's dichotomy: either every subset sum is represented twice, or ∣Σ(A)∣>1+19∣A∣2|\Sigma(A)| > 1 + \frac19|A|^2∣Σ(A)∣>1+91​∣A∣2

Proved
Erdos131.olson_theorem3_2

by moutei · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

abelian-groupsadditive-combinatoricszero-sum

Olson's dichotomy for the set of subset sums, specialised to abelian groups.

For a finite subset A={a1,…,as}A=\{a_1,\dots,a_s\}A={a1​,…,as​} of an abelian group GGG, write

Σ(A)  =  {0,a1}+{0,a2}+⋯+{0,as}  =  {∑x∈Sx  :  S⊆A},\Sigma(A)\;=\;\{0,a_1\}+\{0,a_2\}+\cdots+\{0,a_s\}\;=\;\Big\{\sum_{x\in S}x \;:\; S\subseteq A\Big\},Σ(A)={0,a1​}+{0,a2​}+⋯+{0,as​}={x∈S∑​x:S⊆A},

the set of all subset sums of AAA (the empty subset contributes 000, so 0∈Σ(A)0\in\Sigma(A)0∈Σ(A) always). A representation of g∈Σ(A)g\in\Sigma(A)g∈Σ(A) is a subset S⊆AS\subseteq AS⊆A with ∑x∈Sx=g\sum_{x\in S}x=g∑x∈S​x=g; equivalently, in Olson's notation, a tuple (ε1,…,εs)∈{0,1}s(\varepsilon_1,\dots,\varepsilon_s)\in\{0,1\}^s(ε1​,…,εs​)∈{0,1}s with g=∑iεiaig=\sum_i \varepsilon_i a_ig=∑i​εi​ai​.

The theorem asserts that exactly one of two things can happen, and in either case the set of subset sums is constrained:

  1. every element of Σ(A)\Sigma(A)Σ(A) has at least two distinct representations; or
  2. Σ(A)\Sigma(A)Σ(A) is large:
1+∣A∣29  <  ∣Σ(A)∣.1+\frac{|A|^2}{9}\;<\;|\Sigma(A)|.1+9∣A∣2​<∣Σ(A)∣.

This is Theorem 3.2 of Olson's 1975 paper, which is stated there for an arbitrary — possibly non-abelian, possibly infinite — group GGG and asserts the existence of an arrangement a1,…,asa_1,\dots,a_sa1​,…,as​ of the elements of AAA for which the dichotomy holds, since for a non-abelian group Σ\SigmaΣ depends on the order in which the elements are listed. In an abelian group Σ(A)\Sigma(A)Σ(A) does not depend on the arrangement, so the existential quantifier over arrangements disappears and the statement takes the form above. Olson proves alternative (2) with the sharper constant c=18−O ⁣(log⁡ss)>19c=\tfrac18-O\!\left(\tfrac{\log s}{s}\right)>\tfrac19c=81​−O(slogs​)>91​; the uniform constant 19\tfrac1991​ recorded here is the weaker form that he himself carries through the induction, and is the form in which the theorem is quoted downstream.

On the hypotheses. Olson's statement is about a set of sss distinct non-zero elements, so 0∉A0\notin A0∈/A is kept here even though it is not needed: if 0∈A0\in A0∈A then for every g∈Σ(A)g\in\Sigma(A)g∈Σ(A) and every representation SSS of ggg, exactly one of S∪{0}S\cup\{0\}S∪{0} and S∖{0}S\setminus\{0\}S∖{0} is a second representation, so alternative (1) holds automatically. Nonemptiness of AAA, on the other hand, is genuinely needed: for A=∅A=\varnothingA=∅ one has Σ(A)={0}\Sigma(A)=\{0\}Σ(A)={0}, whose single element 000 has only the representation S=∅S=\varnothingS=∅, so (1) fails, while ∣Σ(A)∣=1=1+029|\Sigma(A)|=1=1+\tfrac{0^2}{9}∣Σ(A)∣=1=1+902​, so (2) fails as well.

Where the dichotomy is used. If AAA is zero-sum-free — no nonempty subset of AAA sums to 000 — then 0∈Σ(A)0\in\Sigma(A)0∈Σ(A) is represented only by S=∅S=\varnothingS=∅, so alternative (1) is impossible and alternative (2) must hold. That deduction is exactly Theorem 7 of Erdős–Lev–Rauzy–Sándor–Sárközy, which is how Olson's theorem enters the bound F(N)<3N+1F(N)<3\sqrt N+1F(N)<3N​+1 for non-dividing sets.

What the proof requires. Olson's proof of Theorem 3.2 is an induction on sss resting on three further results of the same paper: Theorem 2.1 (Kemperman–Scherk: if ∣A+B∣=∣A∣+∣B∣−k|A+B|=|A|+|B|-k∣A+B∣=∣A∣+∣B∣−k then every element of A+BA+BA+B has at least kkk representations as a+ba+ba+b), Theorem 2.2 (if 0∈A0\in A0∈A is finite then for every n≥1n\ge 1n≥1 either nA=⟨A⟩nA=\langle A\ranglenA=⟨A⟩ or ∣nA∣≥∣A∣+(n−1)⌊12(∣A∣+1)⌋|nA|\ge |A|+(n-1)\lfloor\tfrac12(|A|+1)\rfloor∣nA∣≥∣A∣+(n−1)⌊21​(∣A∣+1)⌋), and Lemma 3.1, an averaging estimate on λ(g)=∣(B+g)∩B‾∣\lambda(g)=|(B+g)\cap \overline B|λ(g)=∣(B+g)∩B∣ which feeds Theorem 3.1, the quantitative arrangement theorem. None of these is in Mathlib.

Preamble
import Definitions.Def_Erdos131_NonDividing
import Mathlib.Tactic
open Erdos131
Formal statement
theorem Erdos131.olson_theorem3_2 {G : Type*} [AddCommGroup G] [DecidableEq G]
    (A : Finset G) (hA : A.Nonempty) (h0 : (0 : G) ∉ A) :
    (∀ g ∈ A.powerset.image (fun S => ∑ x ∈ S, x),
        ∃ S ∈ A.powerset, ∃ T ∈ A.powerset,
          S ≠ T ∧ (∑ x ∈ S, x) = g ∧ (∑ x ∈ T, x) = g)
      ∨ 1 + (A.card : ℝ) ^ 2 / 9 < ((A.powerset.image fun S => ∑ x ∈ S, x).card : ℝ) := by sorry
Source
J. E. Olson, 'Sums of sets of group elements', Acta Arith. 28 (1975), 147-156, Theorem 3.2 (p. 151); full text at http://matwbn.icm.edu.pl/ksiazki/aa/aa28/aa2825.pdf. Quoted (for zero-sum-free sets) as Theorem 7 of P. Erdos, V. Lev, G. Rauzy, C. Sandor, A. Sarkozy, 'Greedy algorithm, arithmetic progressions, subset sums and divisibility', Discrete Math. 200 (1999), 119-135.

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me