Skip to content

Erdős problem 541

Let a1,…,apa_1, \dots, a_p be (not necessarily distinct) residues modulo a prime pp, such that there exists some rr so that if S⊆[p]S \subseteq [p] is non-empty and ∑i∈Sai≡0(modp)\sum_{i \in S} a_i \equiv 0 \pmod{p} then ∣S∣=r|S| = r.

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

541.lean

Retained formal statement3 of 3

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

FormalConjectures/ErdosProblems/541.leanErdos541.erdos_541.variants.large_primes4 linesExact file
∀ᶠ (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
SolvedStatement only, no proof