Erdős–Heilbronn conjecture, h = 2 (restricted two-fold sumset)

Proved

ErdosHeilbronn.erdos_heilbronn

by moona3k · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricserdos-heilbronnnumber-theoryrestricted-sumset

Let p be prime and A a nonempty subset of ℤ/p. Then the set of sums a + b of two distinct elements of A has cardinality at least min(p, 2|A| − 3). This is the original h = 2 case of the Erdős–Heilbronn conjecture from 1964, first proved by Dias da Silva and Hamidoune in 1994; it is the restricted analogue of the Cauchy–Davenport theorem, and is sharp for arithmetic progressions.

Preamble

import Mathlib

Formal statement

namespace ErdosHeilbronn

/-- The Erdos-Heilbronn conjecture (1964), h = 2 case, proved by Dias da Silva-Hamidoune (1994):
for nonempty `A ⊆ ℤ/p` with `p` prime, the restricted two-fold sumset
`{a + b // a, b ∈ A, a ≠ b}` has at least `min(p, 2|A| - 3)` elements. -/
theorem erdos_heilbronn {p : ℕ} (hp : p.Prime) {A : Finset (ZMod p)} (hA : A.Nonempty) :
    min p (2 * A.card - 3)
      ≤ (((A.product A).filter (fun ab => ab.1 ≠ ab.2)).image (fun ab => ab.1 + ab.2)).card := by
  sorry

end ErdosHeilbronn

Source

P. Erdős, H. Heilbronn, On the addition of residue classes mod p, Acta Arith. 9 (1964); Dias da Silva–Hamidoune (1994); Alon–Nathanson–Ruzsa (1995/96)

View graph