Back to Problems

erdos_541.variants.general_moduli

Specification

Gao, Hamidoune, and Wang [GHW10] solved this for all moduli `p` (not necessarily prime). [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.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement 
theorem 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
ID: ErdosProblems__541__erdos_541.variants.general_moduli
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.