Erdős Problem 541

References:

• erdosproblems.com/541
• [ErSz76] Erdős, E. and Szemerédi, E., On a problem of Graham. Publ. Math. Debrecen (1976), 123--127.
• [GHW10] Gao, Weidong and Hamidoune, Yahya Ould and Wang, Guoqing, Distinct length modular zero-sum subsequences: a proof of Graham's conjecture. J. Number Theory (2010), 1425--1431.

theorem Erdos541.erdos_541 : True ↔ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (a : Fin p → ZMod p), (∃ (r : ℕ), ∀ (S : Finset (Fin p)), S ≠ ∅ → ∑ i ∈ S, a i = 0 → S.card = r) → (Set.range a).ncard ≤ 2

Let $a_1, \dots, a_p$ be (not necessarily distinct) residues modulo a prime $p$, such that there exists some $r$ so that if $S \subseteq [p]$ is non-empty and $$\sum_{i \in S} a_i \equiv 0 \pmod{p}$$ then $|S| = r$.

Must there be at most two distinct residues amongst the $a_i$?

This was formalized in Lean by Alexeev using Aristotle and ChatGPT.

theorem Erdos541.erdos_541.variants.general_moduli (p : ℕ) (a : Fin p → ZMod p) (ha₀ : ∃ (r : ℕ), ∀ (S : Finset (Fin p)), S ≠ ∅ → ∑ i ∈ S, a i = 0 → S.card = r) : (Set.range a).ncard ≤ 2

Gao, Hamidoune, and Wang [GHW10] solved this for all moduli p (not necessarily prime).

theorem Erdos541.erdos_541.variants.large_primes : ∀ᶠ (p : ℕ) in Filter.atTop, Nat.Prime p → ∀ (a : Fin p → ZMod p), (∃ (r : ℕ), ∀ (S : Finset (Fin p)), S ≠ ∅ → ∑ i ∈ S, a i = 0 → S.card = r) → (Set.range a).ncard ≤ 2

This was proved by Erdős and Szemerédi [ErSz76] for p sufficiently large.